Re: [isabelle] Formalizations of Free Groups and Matrix Groups?

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

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

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.


Joachim Breitner
  e-Mail: mail at
  ICQ#: 74513189
  Jabber-ID: nomeata at

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.