AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

Harmonic heights and the Artin K(π,1) conjecture

Can the mathematical statement in Harmonic heights and the Artin K(π,1) conjecture be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 254)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Harmonic heights and the Artin K(π,1) conjecture'. We prove that the standard Salvetti complex of every Artin group with finitely many standard generators is aspherical. This resolves the Artin K(\pi,1) conjecture in finite rank.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 254). The Lean development was not rebuilt locally.