Update: Aristotle has been used to autoformalize 105 of the 115 Erdős problem formalizations produced by AI tools, i.e. 91% of the total. This includes formalizations of classical proofs such as Pólya (1918), Barrow and Mordell (1937), Hall (1947), de Bruijn (1951), and Lorentz (1954), alongside very recent proofs such as Tao (2026), He–Li–Tang (2026), Pomerance (2026), and Chojecki (2026).
Image from Harmonic (@HarmonicMath)

Apr 8, 2026 · 7:58 AM UTC

6
22
2
163
10,394
RelevantRecentLikes
Source: github.com/teorth/erdosprobl…
AI contributions to Erdős problems

AI contributions to Erdős problems

A community database for the problems on the erdosproblems.com site - teorth/erdosproblems

github.com
1
21
2,448
Great tool!
1
183
People don’t realize how massive this is on its own. Even if you never did any automated theorem proving, autoformalization is a massive leap forward in math
140
Strong translation throughput. Worth naming the line, though: every proof cited — Pólya 1918 through Tao 2026 — is a human proof. Autoformalizing existing arguments and producing novel ones are different problems. Interested in the second metric.
9
Strong translation throughput. Worth naming the line, though: every proof cited — Pólya 1918 through Tao 2026 — is a human proof. Autoformalizing existing arguments and producing novel ones are different problems. Interested in the second metric.
9
I’m using it for quantum + crypto R&D github.com/ChuckGPTX/pqc-fal…
GitHub - ChuckGPTX/pqc-falcon-analysis: Source-grounded audit of IBM Heron Grover claims against...

GitHub - ChuckGPTX/pqc-falcon-analysis: Source-grounded audit of IBM Heron Grover claims against...

Source-grounded audit of IBM Heron Grover claims against Falcon/FN-DSA and ECDSA security language. - ChuckGPTX/pqc-falcon-analysis

github.com
17