Skip to content

The Frontier

Derived view · 5,924 declarations

Every authored declaration in the upstream corpus, typed by the work it actually asks for, computed from exact state rather than read from labels. 2,012 theorems are attackable right now.

Published subset Add a Result
Open obligations
2,862
Settled results
3,062
Problem families
1,055
Lean toolchain
v4.27.0

The shape of the frontier

Settled · kernel 2,834 (47.8%) · compiler-trust 228 · prove 2,012 (34.0%) · state 835 · repair 15

Three kinds of open work

  • 2,012 · Prove: attackable now

    Fully stated theorems whose only hole is the proof. Any prover, human or machine, can attack these today; a success is a genuine advance.

  • 835 · State: instantiate before proving

    answer(sorry) declarations whose statement is itself the unknown. They cannot be proved, only instantiated; standard trust reporting cannot tell these apart from provable targets.

  • 15 · Repair: foundations resting on holes

    Statements that read complete but quantify over objects defined by choice from a sorried existence lemma. Invisible to source inspection; found only by walking the type's transitive closure.

Where the live edge is densest

families by attackable theorems

  • Wikipedia.Transcendental22 prove
  • GreensOpenProblems.1419 prove · 28 state
  • ErdosProblems.9112 prove · 1 state
  • Wikipedia.EllipticCurveRank12 prove
  • ErdosProblems.511 prove · 3 state
  • Paper.MonochromaticQuantumGraph11 prove · 34 state
  • Wikipedia.WallSunSun11 prove
  • ErdosProblems.3610 prove · 3 state
  • ErdosProblems.98710 prove
  • Wikipedia.MovingSofa10 prove
  • ErdosProblems.3499 prove · 3 state
  • ErdosProblems.4949 prove

The 15 foundations to repair

Each rests on an existence lemma proved by sorry, through .choose or Nat.find. Downstream work here builds on sand until the existence proof lands.

  • Erdos1055.erdos_1055.variants.erdos_limit
  • Erdos1055.erdos_1055.variants.selfridge_limit
  • Erdos295.erdos_295.variants.erdos_straus
  • Erdos697.erdos_697.parts.i
  • Erdos697.erdos_697.parts.ii
  • Erdos697.erdos_697.variants.delta_lt
  • Erdos961.erdos_961.variants.erdos_upper_bound
  • Erdos961.erdos_961.variants.jutila_ramachandra_shorey_upper_bound
  • MovingSofa.sofaConstant_eq
  • MovingSofa.sofaConstant_eq_volume_gerversSofa
  • MovingSofa.volume_eq_sofaConstant_iff_congruent_gerversSofa
  • OeisA87719.a_1
  • OeisA87719.a_2
  • OeisA87719.a_3
  • OeisA87719.a_formula

Exact-state provenance

Derived and disposable, rebuilt from its census.

corpus williamjblair/formal-conjectures @ e51535ae2cae (≡ google-deepmind/formal-conjectures@9f5ee773)
census sha256:852464170329dc4b452bf05be4778a46adb6562b110b9c31bb492df56102e81d · measured 2026-08-23