Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topic: new results in graph theory.


Jeremy Avigad (May 26 2021 at 13:17):

A colleague of mine pointed me to this article: https://www.newscientist.com/article/2278276-an-ai-has-disproved-five-mathematical-conjectures-with-no-human-help
It's behind a firewall, but the paper and the code are freely available on the author's website: http://www.math.tau.ac.il/~adamwagner/index.html
It's the first paper listed. It looks really impressive to me...

Kevin Buzzard (May 26 2021 at 13:23):

I think someone posted Gowers' tweet about it in another thread. What I like about it is that they got the AI to look for potential counterexamples and then they actually looked at the output -- the graphs which the AI thought were promising -- and spotted the patterns and then went on to find the actual counterexamples themselves. They were lucky that the counterexamples had some structure.

Kevin Buzzard (May 26 2021 at 13:23):

There are other proofs in graph theory which use random techniques, i.e. estimates to show that a probability that a graph with a million nodes has property X is a little less than 1, and hence there must be some counterexample

Kevin Buzzard (May 26 2021 at 13:24):

https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning.20for.20Theorem.20Proving/topic/RL.20finds.20counterexamples.20to.20open.20problems.20in.20graph.20theory/near/238877949


Last updated: Dec 20 2023 at 11:08 UTC