open
Theoretical Computer Science
The mathematics of computation: what can be computed, at what cost, and with what guarantees. Machine models, complexity classes, algorithm…
83 of 505 targeted · 24 topics
AFTD An open research programme
Auto-Formalizing Theoretical Domains
Open proof to the community.
Open verdict by the community.
A machine that reads a curriculum of the theoretical sciences, states their theorems in Lean 4, proves them against Mathlib, and publishes whatever Lean accepts — immediately, to everyone, with no paper and no author line. Nothing is here because a language model said it was true.
The diagonal halting problem is not computable.
/-- The diagonal halting problem is undecidable (not computable). -/ theorem self_halting_problem_undecidable : ¬ComputablePred (fun c : Nat.Partrec.Code => (Nat.Partrec.Code.eval c (Encodable.encode c)).Dom) := by intro h obtain ⟨_, hc⟩ := h let f : Nat.Partrec.Code → ℕ →. ℕ := fun c _ => cond (decide (Nat.Partrec.Code.eval c (Encodable.encode c)).Dom) Part.none (Part.some 0) have hf : Partrec₂ f := Partrec.cond (hc.comp Computable.fst) Partrec.none (Computable.const 0).partrec obtain ⟨c, e⟩ := Nat.Partrec.Code.fixed_point₂ hf have e_app := congr_fun e (Encodable.encode c) dsimp [f] at e_app by_cases H : (Nat.Partrec.Code.eval c (Encodable.encode c)).Dom · have h_none := e_app ▸ H simp [H] at h_none · apply H rw [e_app] simp [H]
115machine-verified declarations82 theorems · 33 definitions
18topics with resultsacross 3 of 6 domains
1,035declarations in the curriculum49 topics, 6 domains
$21API spend to dateabout 19¢ per verified declaration
Point a loop at a curriculum of theoretical domains. Let it state and prove, forever. Keep only what Lean accepts. Publish all of it, immediately, to everyone.
Theory is written to be read by people, and it is checked by people. That checking is the bottleneck: it does not scale, it is unevenly spread across subjects, and most of it is never written down in a form another person or machine can reuse.
Lean 4 and Mathlib remove the bottleneck for the checking.
AFTD automates the other half — deciding what is worth stating,
writing the statement, attempting the proof — a subject at a time, not
a paper at a time. The unit of progress is one Lean declaration that anyone
can import tomorrow.
How it works
Three agents, one dependency graph, and Lean as the only judge
- 1
Propose
The Proposer works one topic at a time: it transcribes known results from the literature and proposes its own — generalizations, converses, bridges between topics.
- 2
Round-trip
One model reads only the Lean and says what it asserts; another reads only the English and formalizes it blind. Lean is asked first whether the two agree.
- 3
Prove
The Prover takes one statement at a time. When it is stuck it files the lemmas it needs and the graph grows a rung — it never quietly proves something weaker.
- 4
Publish
Lean elaborates it,
#print axiomsis clean, and it goes public with its full source, rebuildable by anyone withlake build.
The scheduler is not a language model. What to work on, when to give up and when to split a hard theorem into lemmas are deterministic rules over the graph; the models supply judgement, never control flow.
The curriculum
Six theoretical domains
3 are open so far; the rest are waiting on compute, not on code.
waiting on compute
Optimization & Operations Research
The theory of optimizing over structured sets: when an optimum exists, when it is certified by a dual object, and how fast an iterative method…
0 of 115 targeted · 5 topics
waiting on compute
Probability & Mathematical Statistics
Measure-theoretic probability and the theory of statistical inference: limit behaviour, concentration, what an estimator can achieve, and what no…
0 of 135 targeted · 6 topics
waiting on compute
Mathematical Logic & Foundations
The mathematics of formal systems themselves: what structures satisfy a theory, what a proof system can and cannot prove, and the set-theoretic…
0 of 75 targeted · 4 topics
open
Game Theory & Mathematical Economics
Strategic interaction and the theory of collective decisions: when equilibria exist, what aggregation rules are possible, and what mechanisms can be…
16 of 95 targeted · 5 topics
open
Theoretical Physics
The mathematical structure of physical theory: the variational principles that generate the equations of motion, the symmetries that constrain them,…
16 of 110 targeted · 5 topics
Take part
Pose, read, judge
01
Pose a problem
Send a statement through a GitHub issue. Once reviewed, the machine formalizes it, checks the formalization says what you said, and tries to prove it. Your handle stays on it.
How submitting works →02
Read the proofs
Every verified declaration has its own page: the statement in words and in Lean, the full proof, what it builds on and what builds on it.
The knowledgebase →03
Judge the verdicts
Correctness is settled by Lean. Everything else is yours to dispute: a name that claims too much, a trivial statement, a definition the subject would not recognise.
Challenge a result →Community problems
All problems →No community problems yet. Pose the first one: a statement from any of the six domains, with a reference if you have one.
Submit a problemRecently verified
Knowledgebase →For any unitary continuous linear operator U on a complex Hilbert space E and any vectors ϕ and ψ in E, the inner product is preserved: ⟪U ϕ, U ψ⟫_ℂ = ⟪ϕ, ψ⟫_ℂ.
For any orthogonal projection operator P (a self-adjoint idempotent continuous linear map) on a complex Hilbert space E and any state vector ψ in E, the inner product ⟪ψ, P ψ⟫_ℂ equals the complex square of the norm ‖P ψ‖.
The constant zero trajectory is a Hamiltonian trajectory for the zero Hamiltonian.
is_lorentz_matrix_onetheorem
The 4x4 identity matrix is a Lorentz matrix.
is_lorentz_matrix_multheorem
If A and B are 4x4 Lorentz matrices, then their matrix product A * B is also a Lorentz matrix.
What “proved” means here
- Lean elaborates it against Mathlib, with zero errors.
#print axiomsis clean: nothing beyondpropext,Classical.choice,Quot.sound— which rules outsorry,native_decideand any axiom an agent declared for itself.- It survives the round trip: the Lean and the English are each read blind and must agree.
- Its name claims no more than it proves, and it does not privately re-invent a concept Mathlib already has.
What this is not
It is not an attempt on open problems, and not a claim that mathematicians are replaceable. Most of the knowledgebase is known mathematics, carefully transcribed and machine-checked, plus a growing minority of modest original statements. The value is in the aggregate — verified, open and cumulative — not in any single line of it.
No one on this side takes an author line, and there will be no paper.
The only real cost is tokens.
Fund the run with API credits and you are acknowledged on the results — specifically: what you gave, what was spent, and which verified results your money paid for. Money buys attempts, not results; a name on the board is support, not authorship.