Zulip Chat Archive

Stream: general

Topic: AITP


view this post on Zulip Johan Commelin (Oct 02 2018 at 14:25):

Here is a conference on AI and Theorem Proving: http://aitp-conference.org/2019/
The co-chair, Josef Urban, just told me that his ML system can now prove about 50% of Mizar's library.

view this post on Zulip Johan Commelin (Oct 02 2018 at 14:25):

I really wish that we could interface with that system, and have it write 50% of our proofs for us.

view this post on Zulip Patrick Massot (Oct 02 2018 at 14:33):

Asking google about Josef Urban doesn't immediately leads to what I was looking for...

view this post on Zulip Johan Commelin (Oct 02 2018 at 14:34):

@Scott Morrison @Keeley Hoek I think this might be really interesting for you. If you want I can put you in touch with Josef.

view this post on Zulip Johan Commelin (Oct 02 2018 at 14:34):

@Patrick Massot http://cs.ru.nl/~urban/

view this post on Zulip Patrick Massot (Oct 02 2018 at 14:35):

I found it eventually, although google thinks this is less interesting that marathon runner having clothing issues

view this post on Zulip Scott Morrison (Oct 02 2018 at 21:54):

I may try to go. I met Josef at Dagstuhl.

view this post on Zulip Jeremy Avigad (Apr 14 2019 at 21:50):

@Kevin Buzzard mentioned AITP. I'd be curious to hear his or anyone's take on the highlights of the meeting.

view this post on Zulip Kevin Buzzard (Apr 14 2019 at 21:56):

It was mostly people using ATPs not ITPs. TPTP got mentioned a lot more than Coq or Lean. Isabelle got more of a look-in. A lot of the slides for the talks are now available online. I was permanently confused by the people who were producing data of the following form: "We took a dataset of lots of theorems, trained our AI on 70% of them and then saw how it did on the rest; it solved 56% of them". And I would say "yeah but which ones? Did it solve any hard ones? Did it solve precisely all the ones which had two line proofs? What about all the theorems in the test data which were trivial corollaries of the stuff in the training data? Which statements did your deep learning neural net or whatever it is actually _solve_?" but they didn't think that way -- for them the theorems are just a database. I don't think they have favourite theorems :-)

Some people from google were writing a system-agnostic theorem prover; one of them told me that computers would be better than humans at maths within 10 years. Not everyone believed this. But the argument for it is apparently "look at computer vision -- everyone said it was completely impossible 20 years ago but now we have self-driving cars".

view this post on Zulip Reid Barton (Apr 14 2019 at 22:16):

I have heard similar claims from AI people and I'm not sure whether to assign more weight to the fact that they know more about AI than I do or the fact that I know more about math than they do.

view this post on Zulip Kevin Buzzard (Apr 14 2019 at 22:19):

I have heard similar claims from AI people and I'm not sure whether to assign more weight to the fact that they know more about AI than I do or the fact that I know more about math than they do.

Yes, these were pretty much my feelings too.

view this post on Zulip Kevin Buzzard (Apr 14 2019 at 22:34):

The google people put up a website for their work at https://sites.google.com/view/holist/home . It was Christian Szegedy, one of the authors of the paper, who said to me that computers will be better than humans within 10 years. He has a PhD in some discrete maths area.

view this post on Zulip Kevin Buzzard (Apr 14 2019 at 22:36):

I asked them about whether they could use Lean -- they looked at it 2 years ago but I told them that a lot had changed since then. They said their methods should be applicable to any theorem prover.

view this post on Zulip Jeremy Avigad (Apr 14 2019 at 22:45):

Thanks for the summary. I agree that the progress to date seems fairly limited, and mathematics seems to have a very different character from domains where ML has been successful. But I also wonder whether I am missing something. That's why I was curious to hear about the meeting.

By the way, Szegedy is co-author on a number of papers that are highly cited. (https://scholar.google.com/citations?user=3QeF7mAAAAAJ&hl=en.) It is amazing to me that a paper that is only four years old can have more than 12,000 citations.

view this post on Zulip Chris Hughes (Apr 14 2019 at 22:50):

Even if it doesn't prove the Riemann hypothesis, it might become better at filling in the easy bits than humans, and make formal proof realistic for research maths.

view this post on Zulip Kevin Buzzard (Apr 15 2019 at 07:14):

That seems like a far more realistic goal


Last updated: May 15 2021 at 02:11 UTC