This page may contain stale information. Last updated: 2026-08-01
Definition
Use of AI systems to discover, prove, disprove, or formalize mathematical results — spanning informal conjecture search, proof generation, and machine-checkable lean-formalization.
Key Points
- 2026-08-01: openai-astra ten decade-open problems with Lean certificates (2026-08-01-openai-astra-ten-math-advances)
- 2026-05: OpenAI Erdős unit-distance disproof (unit-distance-problem)
- Cost framing: ~$2,000 Sol API rates for Astra ten-pack search
- Attribution ethics: Leiden declaration — do not claim pure human authorship for AI-generated arguments
Related
- lean-formalization
- automated-theorem-proving
- openai-astra
- openai-astra-frontier
- ai-for-science
- openai