Primary evidence
- Solution of the Robbins ProblemS1 · Primary research · Paper
EQP finds a proof resolving the Robbins conjecture
The automated search produced a compact equational derivation in a problem that had resisted prior human and machine efforts for decades.
What happened?
On 10 October 1996, William McCune's EQP found a proof showing that Robbins algebras are Boolean; the proof was subsequently checked with the Otter theorem prover and studied by mathematicians.
Why it matters
The event supplied early evidence that automated theorem proving could contribute directly to unresolved mathematics, a central ambition of modern AI4Math.
Significance rationale: EQP's Robbins-algebra proof is a landmark case in which an automated theorem prover produced the key proof of a long-standing open algebraic question, demonstrating ATP as a tool for new mathematical results rather than only benchmark reproving.
Historical context
Earlier developments
—
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- AI primary, human verified
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- New proof
- Interface
- Formal, Symbolic
- AI contribution
- EQP autonomously searched for and found the formal proof; separate automated checking and human mathematical inspection followed.
- Human contribution
- William McCune developed the prover and search setup; mathematicians contextualized, simplified and communicated the machine-found proof.
- Verification
- Paper released · E3 · Inspectable artifact · Machine-checked
- Last reviewed
- 2026-09-15
Technical details
- Systems
- eqp, otter
- Organizations
- argonne-national-laboratory
- Problems
- robbins-conjecture
- Methods
- equational-theorem-proving, automated-proof-search
Sources & artifacts
- Solution of the Robbins ProblemS1 · Primary research · Paper · accessed 2026-09-15
- EQP Robbins proof record in the Argonne reportArtifact · Proof artifact
Verification history
- 1996-10-10 · Paper released · E3 · Inspectable artifact
The Argonne technical report records the EQP proof and subsequent Otter verification; machine checking does not convert Chronicle into an independent mathematical-priority arbiter.
Corrections
No corrections recorded.