14
votes
Successes of machine learning in formal theorem proving
Only a bit more than two months ago, a new formula for Kazhdan-Lusztig
polynomials was found by Google's deep learning subsidiary: DeepMind (the same machine-learning company that wrote AlphaGo to ...
- 1,175
11
votes
Accepted
auto-generating the proof of infinitude of primes
I doubt you are out of date. I think given a reasonable interpretation of this question, this is well beyond current (2022) systems.
Nonetheless, I will also argue your question needs some ...
- 10.3k
8
votes
Successes of machine learning in formal theorem proving
The group at OpenAI has recently published a new paper, among other problems they have been able to prove two questions from the International Mathematical Olympiad. Isabelle's Sledgehammer has been ...
- 665
7
votes
Accepted
What are some automated theorem generators? What background logic do they use and what heuristics do they use for theorem-goodness?
MetaGen may be unique in that it is a Neural Theorem Generator which generates both statements and proofs.
Nonetheless, there are a number of other papers which do 2 of the 3: Neural, Generate ...
- 10.3k
Only top scored, non community-wiki answers of a minimum length are eligible