*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Formalizations of Free Groups and Matrix Groups?*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Mon, 10 May 2010 11:34:15 +0200*In-reply-to*: <q2gcc2478ab1005080940yc3652e94r557a2ecea600e821@mail.gmail.com>*References*: <1273267675.11358.4.camel@kirk> <q2gcc2478ab1005080940yc3652e94r557a2ecea600e821@mail.gmail.com>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Hi Brian, thanks for your reply. Am Samstag, den 08.05.2010, 09:40 -0700 schrieb Brian Huffman: > Then you could define a function analogous to "lists" with type "'a > set => 'a free_group set" that would pick out the values generated by > some smaller set. This would probably make a nice AFP entry, if you > wanted to formalize it. I’m tempted to do so, once I’m more familiar with Isar syntax. After doing more research, I also found http://isarmathlib.org/ This poses a new question: What foundation should I use? As a mathematician, I’d first say that set theory is the correct base to formalize pure math on – but does it really matter? Will I have problems convincing other mathematician to trust a formalized proof on Higher Logic? Are the provable theorems within, say, pure algebra the same in either systems, just with different proofs? If so, is this fact proven? Or is it indeed necessary to prove results in either system? Does the AFP also accept Isabelle/ZF submissions? As a side note: One of my hopes when getting interested in theorem provers and proof checkers was that I’d get a tool that can also investigate proof. For example, tell me whether a certain proof uses the axiom of choice or not. It seems that the Metamath system allows for that, but is otherwise very laborious to use. To pick up the recent discussion about proof certificates and stability: Has there been done work or thought in the direction of exporting Isabelle proof objects into Metamath proofs? It seems to me that this would provide for inspectable and stable proofs, while exploiting the power of Isabelle and ease of Isar. Greetings, Joachim -- Joachim Breitner e-Mail: mail at joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata at joachim-breitner.de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Formalizations of Free Groups and Matrix Groups?***From:*Brian Huffman

**Re: [isabelle] Formalizations of Free Groups and Matrix Groups?***From:*Tobias Nipkow

**References**:**[isabelle] Formalizations of Free Groups and Matrix Groups?***From:*Joachim Breitner

**Re: [isabelle] Formalizations of Free Groups and Matrix Groups?***From:*Brian Huffman

- Previous by Date: Re: [isabelle] name of locale predicate
- Next by Date: Re: [isabelle] name of locale predicate
- Previous by Thread: Re: [isabelle] Formalizations of Free Groups and Matrix Groups?
- Next by Thread: Re: [isabelle] Formalizations of Free Groups and Matrix Groups?
- Cl-isabelle-users May 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list