AITP

Stream: general

[Johan Commelin]

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.

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Scott Morrison]

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

[Jeremy Avigad]

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

[Kevin Buzzard]

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".

[Reid Barton]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Jeremy Avigad]

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.

[Chris Hughes]

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.

[Kevin Buzzard]

That seems like a far more realistic goal