Mathematicians who use proof assistants

[Martin Escardo]

We know that many computer scientists and (probably fewer) logicians use
proof assistants.

Can we start to compile a list of mathematicians who use, or have used,
or intend to use proof assistants?

(Of course, the boundaries of computer science/logic/mathematics are
largely artificial, and the group of people addressed here witness that,
but let's not dwell on this in this thread.)

(As far as I know, Tim Gowers hasn't used proof assistants, but he has
given many talks about what he sees as the future role of computers in
mathematics (I attended two). Such mathematicians can be included too in
our compilation, if you know of any.)

If you send names and links, publicly or privately, I can try to produce
a summary after a while. Do send the obvious ones too, please.

Best,
Martin

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Peter LeFanu Lumsdaine]

Slightly on a tangent: regarding Tim Gowers, those who haven’t already seen them may be interested by these recent blog posts of his.  They discuss a program he’s been working on with Mohan Ganesalingam, which is a bit difficult to paraphrase but which I guess I’d gloss as essentially a somewhat unconventional proof assistant/automated theorem prover:

http://gowers.wordpress.com/2013/04/02/a-second-experiment-concerning-mathematical-writing/

http://gowers.wordpress.com/2013/04/14/answers-results-of-polls-and-a-brief-description-of-the-program/

(So perhaps this would qualify him as a mathematician who uses proof assistants?)

–p.

--
You received this message because you are subscribed to the Google Groups "IAS Univalent Foundations" group.
To unsubscribe from this group and stop receiving emails from it, send an email to univalent-foundations+unsub...@googlegroups.com.
To post to this group, send email to univalent-foundations@googlegroups.com.
Visit this group at http://groups.google.com/group/univalent-foundations?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.

[Martin Escardo]

This is not tangential! Nice.

M.

> univalent-foundat...@googlegroups.com
> <mailto:univalent-foundations%2Bunsu...@googlegroups.com>.

> To post to this group, send email to

> univalent-foundations@__googlegroups.com
> <mailto:univalent-...@googlegroups.com>.
> Visit this group at
> http://groups.google.com/__group/univalent-foundations?__hl=en
> <http://groups.google.com/group/univalent-foundations?hl=en>.
> For more options, visit https://groups.google.com/__groups/opt_out
> <https://groups.google.com/groups/opt_out>.

[Andrej Bauer]

Gower's work reminds me of Bruno Buchberger's work from a while ago, and Analytica before that.

In any case, I like the idea. We should send out a question to mathematicians:

Are you now, or have you ever been a member of the Proof Assistant Party?

That is bound to get a response.

    univalent-foundations+__unsub...@googlegroups.com

    <mailto:univalent-foundations%2Bunsu...@googlegroups.com>.

    To post to this group, send email to

    univalent-foundations@__googlegroups.com

    <mailto:univalent-foundations@googlegroups.com>.

    Visit this group at
    http://groups.google.com/__group/univalent-foundations?__hl=en
    <http://groups.google.com/group/univalent-foundations?hl=en>.
    For more options, visit https://groups.google.com/__groups/opt_out
    <https://groups.google.com/groups/opt_out>.

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

--
You received this message because you are subscribed to the Google Groups "IAS Univalent Foundations" group.

To unsubscribe from this group and stop receiving emails from it, send an email to univalent-foundations+unsub...@googlegroups.com.
To post to this group, send email to univalent-foundations@googlegroups.com.
Visit this group at http://groups.google.com/group/univalent-foundations?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.

[Bas Spitters]

When reading the post, I was wondering whether such an idea could be used in the future to translate between HoTT and informal HoTT.
There is also "weak type theory" developed from the automath project.
It is a formal language, but looks somewhat like natural language.

http://alexandria.tue.nl/extra1/wskrap/publichtml/200205.pdf

To unsubscribe from this group and stop receiving emails from it, send an email to univalent-founda...@googlegroups.com.
To post to this group, send email to univalent-...@googlegroups.com.