formal-verification
Three Days On, Nobody Has Publicly Compiled OpenAI's Ten Proofs News
OpenAI's repository of Lean proofs for ten mathematics results has 434 stars and 39 forks but exactly one commit, no pull requests, and no issues, and no third party has published a build log showing the proofs check.
The non-sofic group is the one OpenAI claim a computer can check News
Chapter 3 of OpenAI's new manuscript claims to have constructed a non-sofic group, settling a long-open question, and ships roughly 34,000 lines of Lean code with no unproved placeholders so outsiders can verify it.
OpenAI publishes ten mathematics claims with Lean proofs and no named authors News
OpenAI released ten claimed advances in mathematics and theoretical computer science today, produced by an unreleased internal model it calls Astra, with a 249-page manuscript collection and machine-checkable proofs for every result.
Terence Tao says the bottleneck in AI-assisted mathematics is understanding, not proofs News
In an ICM public lecture, Terence Tao argues that AI and formal proof systems accelerate generating and verifying proofs but not explaining, reviewing or canonicalizing them, so correct results could pile up faster than the field can absorb them.
Proof assistants: why a machine-checked proof beats a convincing one Lesson
A proof assistant is software like Lean or Coq that checks a mathematical proof step by step against strict logical rules, so a proof is accepted only if the machine confirms every inference -- which is exactly why the field demands them when an AI claims to have proved a theorem.