SI Report-Harmonic Aristotle Automated Theorem Prover
DOI:
https://doi.org/10.70777/si.v3i3.18760Keywords:
automated theorem prover, code verification, open math problems, erdos problem, historic math problems, verina benchmarkAbstract
A description of the tool used by OpenAI's internal model to prove 100+ open math problems (as claimed by OpenAI).
References
[1] Aristotle: IMO-level Automated Theorem Proving. Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern-Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, Martin Michelsen, Riley Patterson, Eric Rodriguez, Laura Scharff, Vikram Shanker, Vladmir Sicca, Hari Sowrirajan, Aidan Swope, Matyas Tamas, Vlad Tenev, et al., arXiv:2510.01346 [cs.AI], 2025. License: Creative Commons Attribution 4.0 International (CC BY 4.0).
[2] Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem. Gabriel Rongyang Lau, arXiv:2605.20120 [cs.AI], 2026. License: Creative Commons Attribution 4.0 International (CC BY 4.0); Pagination: 11 pages (arXiv preprint).
[3] Harmonic's AI Aristotle Claims Solution to Historic Math Puzzle. Mindplex Magazine, 2025. News and analysis report detailing Boris Alexeev's deployment of Aristotle on Erdős Problem 124 and the distinction between the solved variant and the original conjecture. License: Proprietary / Editorial web publication.
[4] Aristotle Learns to Code, Achieving New State-of-the-Art of 96.8% on Code Verification Benchmark. Harmonic Research Announcements, 2026. Technical overview of Aristotle's verification performance on the VERINA benchmark. License: Proprietary / Corporate technical release.
Downloads
Published
How to Cite
Issue
Section
Categories
License
Copyright (c) 2026 Kris Carlson
This work is licensed under a Creative Commons Attribution 4.0 International License.
