Mazur Theoremformalization programme

Open, kernel-checked mathematics · Lean 4

Mazur’s theorem, one verified dependency at a time.

A public programme for the exact Lean Pool target: the rational torsion set of an elliptic curve over ℚ has ncard at most 16. The hard part is not hidden: every theorem, interface, dependency, and integration boundary is on the board.

Find a challengeRead the blueprint
Checked Lean
89,307 lines
Compiled modules
175
Open contracts
8 boundaries · 113 pts

Programme principleProgress is earned by use, not by volume: a definition reaches 100% only when its proof is checked, its API is accepted, and a downstream theorem consumes it.

The weighted roadmap

A dependency graph with an honest denominator.

The programme totals 1000 points. Stage weights estimate effort across the whole theorem—not file counts, issue counts, or perceived mathematical elegance.

Stage contract

What this stage must define and prove

These are the concrete APIs and results that count as this stage’s scope. Node cards below show how the work is divided and connected.

  • definitionIntegrated
    MazurTorsion.RationalTorsion

    The rational torsion subgroup used by every downstream cardinality and point-order theorem.

  • definitionIntegrated
    MazurTorsion.cyclicOrders and remainingKubertForbiddenOrders

    The exact allowed cyclic orders and the four composite callbacks still exposed by the baseline.

  • theoremIntegrated
    MazurTorsion.rationalTorsion_orders_mem_cyclicOrders_of_remaining_obstructions

    The compiled point-order reduction with only prime orders at least 11 and orders 18, 25, 35, and 49 left open.

  • theoremIntegrated
    MazurTorsion.torsion_ncard_le_of_explicit_arithmetic

    The exact ncard-at-most-16 target once every rational torsion point has an allowed order.

All 1 dependency nodes

50.0 of 50 points integrated
Done50 pts

Finite-group classification and cardinality assembly; full 2-, 3-, 4-, 5-, and 7-torsion obstructions; exceptional products; and unconditional exclusions of orders 14, 15, 16, 20, 21, 24, and 27.

  • definitionIntegrated
    MazurTorsion.RationalTorsion

    The rational torsion subgroup on which the point-order and cardinality reductions are stated.

    MazurTorsion.GroupTheory.ClassificationCardinality
  • definitionIntegrated
    MazurTorsion.cyclicOrders

    The finite set of cyclic point orders allowed by the target classification.

    MazurTorsion.GroupTheory.ClassificationCardinality
  • definitionIntegrated
    MazurTorsion.remainingKubertForbiddenOrders

    The exact residual composite-order callbacks exposed by the imported baseline.

    MazurTorsion.Arithmetic.PointOrder
  • theoremIntegrated
    MazurTorsion.rationalTorsion_orders_mem_cyclicOrders_of_remaining_obstructions

    The checked point-order reduction from the remaining prime and composite exclusions.

    MazurTorsion.Arithmetic.PointOrder
  • theoremIntegrated
    MazurTorsion.torsion_ncard_le_of_explicit_arithmetic

    The checked cardinality bound once the explicit point-order hypotheses are supplied.

    MazurTorsion.Arithmetic.CardinalityReduction
Needs
foundation node
Unlocks

Interactive dependency graph

Every node, edge, and hand-off.

Read left to right across the six programme stages. Select any node to inspect its definitions, theorem contracts, dependencies, and downstream consumers.

Graph focus
Integrated Open Planned or blocked
Mazur theorem dependency graph48 formalization nodes arranged in 6 stage columns. Select a node to inspect its exact scope.Integrated baseline01 · Integrated baseline1 nodes · 50 ptsFinite-level endpoints02 · Finite-level endpoints8 nodes · 100 ptsShared algebraic geometry and isogenies03 · Shared geometry13 nodes · 300 ptsPrime-level infrastructure04 · Prime infrastructure14 nodes · 400 ptsMazur's prime-order argument05 · Prime argument8 nodes · 100 ptsIntegration and hardening06 · Integration4 nodes · 50 ptsImported sorry-free Mazur baselineMT-BASE-INTEGRATED50 pts · DoneThe five-coset bound on X_1(11)MT-X11-COSET12 pts · OpenExclude exact rational order 11MT-X11-JOIN2 pts · BlockedClassify the noncuspidal rational points on X_1(13)MT-X13-NONCUSP26 pts · Research OpenClassify the noncuspidal rational points on the order-18 curveMT-X18-NONCUSP18 pts · Research OpenExclude exact rational order 25MT-O25-EXCLUDE16 pts · Research OpenExclude exact rational order 35MT-O35-EXCLUDE14 pts · Research OpenBridge exact order 49 to the X_0(49) correspondenceMT-O49-TOWER10 pts · OpenAssemble all finite-level exclusionsMT-FINITE-JOIN2 pts · BlockedFinite support of orders of rational functionsMT-TC-A1-ORDER-SUPPORT15 pts · OpenDegree-zero product formula on a proper smooth curveMT-TC-A2-PRODUCT-FORMULA15 pts · BlockedDimension of a product of abelian varietiesMT-TC-E0-PRODUCT-DIM2 pts · OpenDivisor-line-bundle dictionaryMT-TC-A3-DIVISOR-LINE-BUNDLE18 pts · BlockedCoherent cohomology of proper curvesMT-TC-B1-COHERENT-COHOMOLOGY35 pts · BlockedRiemann-Roch and Serre duality for curvesMT-TC-B2-RR-SERRE25 pts · BlockedRelative cohomology and base changeMT-TC-C1-RELATIVE-COHOMOLOGY30 pts · BlockedRelative effective divisors and symmetric powersMT-TC-C2-SYMMETRIC-POWERS15 pts · BlockedRigidified relative Picard functorMT-TC-D1-PICARD-FUNCTOR35 pts · BlockedRepresentability and properness of Pic^0MT-TC-D2-PICARD-REPRESENTABILITY45 pts · BlockedJacobian variety and sanity checksMT-TC-E1-JACOBIAN-VARIETY20 pts · BlockedAbel-Jacobi universal property and base changeMT-TC-F1-ABEL-JACOBI20 pts · BlockedElliptic-curve isogenies, quotients, duals, and Weil pairingMT-EC-ISOGENY-WEIL25 pts · PlannedNeron models over discrete valuation ringsMT-NERON-BASE40 pts · BlockedIdentity components and component groupsMT-NERON-COMPONENTS30 pts · BlockedTorsion specialization through Neron modelsMT-NERON-SPECIALIZATION30 pts · BlockedFinite-flat commutative group schemesMT-FFGS-BASIC20 pts · PlannedConnected-etale sequenceMT-FFGS-CONNECTED-ETALE20 pts · BlockedOort-Tate classification and Raynaud uniquenessMT-FFGS-OORT-RAYNAUD40 pts · BlockedThe Gamma_0 modular-curve moduli problemMT-X0-MODULI30 pts · PlannedIntegral compactified X_0(N)MT-X0-INTEGRAL30 pts · BlockedCusps and the rational cusp divisorMT-X0-CUSPS20 pts · BlockedThe modular Jacobian J_0(N)MT-X0-JACOBIAN20 pts · BlockedHecke correspondences on J_0(N)MT-X0-HECKE30 pts · BlockedThe Eisenstein ideal and Hecke quotientMT-X0-EISENSTEIN-ALGEBRA30 pts · BlockedArithmetic of the Eisenstein quotientMT-X0-EISENSTEIN-QUOTIENT40 pts · BlockedCyclotomic unramified character extensionsMT-CYCLOTOMIC-UNRAMIFIED20 pts · PlannedPrime torsion forces semistabilityMT-PRIME-SEMISTABLE10 pts · BlockedTorsion specializes outside identity componentsMT-PRIME-OUTSIDE-IDENTITY10 pts · BlockedSpecialize through the Eisenstein quotientMT-PRIME-EISENSTEIN-SPECIALIZATION20 pts · BlockedThe division-field extension is everywhere unramifiedMT-PRIME-DIVISION-FIELD15 pts · BlockedExclude the inverse-cyclotomic extensionMT-PRIME-HERBRAND-KUMMER10 pts · BlockedSplit the p-torsion extensionMT-PRIME-SPLIT-SEQUENCE10 pts · BlockedShafarevich finiteness for the isogeny chainMT-PRIME-SHAFAREVICH15 pts · BlockedThe infinite isogeny-chain contradictionMT-PRIME-ISOGENY-CHAIN10 pts · BlockedConverge on a shared Mathlib and Tau Ceti pinMT-PIN-MIGRATION20 pts · PlannedIntegrate finite and prime point-order APIsMT-API-INTEGRATION10 pts · BlockedKernel-check Mazur's torsion boundMT-FINAL-ASSEMBLY15 pts · BlockedFinal exposition, provenance, and reproducibility auditMT-EXPOSITION-AUDIT5 pts · Blocked
Browse the graph as a dependency list
  1. Integrated baseline
    • Foundation node
  2. Finite-level endpoints
    • Needs MT-BASE-INTEGRATED
    • Needs MT-X11-COSET
    • Needs MT-BASE-INTEGRATED
    • Needs MT-BASE-INTEGRATED
    • Needs MT-BASE-INTEGRATED
    • Needs MT-BASE-INTEGRATED
    • Needs MT-BASE-INTEGRATED
    • Needs MT-X11-JOIN, MT-X13-NONCUSP, MT-X18-NONCUSP, MT-O25-EXCLUDE, MT-O35-EXCLUDE, MT-O49-TOWER
  3. Shared algebraic geometry and isogenies
    • Needs MT-BASE-INTEGRATED
    • Needs MT-TC-A1-ORDER-SUPPORT
    • Needs MT-BASE-INTEGRATED
    • Needs MT-TC-A2-PRODUCT-FORMULA
    • Needs MT-TC-A3-DIVISOR-LINE-BUNDLE
    • Needs MT-TC-B1-COHERENT-COHOMOLOGY
    • Needs MT-TC-B1-COHERENT-COHOMOLOGY
    • Needs MT-TC-A3-DIVISOR-LINE-BUNDLE, MT-TC-C1-RELATIVE-COHOMOLOGY
    • Needs MT-TC-A3-DIVISOR-LINE-BUNDLE, MT-TC-C1-RELATIVE-COHOMOLOGY
    • Needs MT-TC-B2-RR-SERRE, MT-TC-C2-SYMMETRIC-POWERS, MT-TC-D1-PICARD-FUNCTOR
    • Needs MT-TC-D2-PICARD-REPRESENTABILITY, MT-TC-E0-PRODUCT-DIM
    • Needs MT-TC-C1-RELATIVE-COHOMOLOGY, MT-TC-E1-JACOBIAN-VARIETY
    • Needs MT-BASE-INTEGRATED
  4. Prime-level infrastructure
    • Needs MT-TC-E1-JACOBIAN-VARIETY, MT-EC-ISOGENY-WEIL
    • Needs MT-NERON-BASE
    • Needs MT-NERON-COMPONENTS
    • Needs MT-BASE-INTEGRATED
    • Needs MT-FFGS-BASIC
    • Needs MT-FFGS-CONNECTED-ETALE
    • Needs MT-BASE-INTEGRATED
    • Needs MT-X0-MODULI
    • Needs MT-X0-INTEGRAL
    • Needs MT-X0-INTEGRAL, MT-TC-E1-JACOBIAN-VARIETY, MT-TC-F1-ABEL-JACOBI
    • Needs MT-X0-JACOBIAN, MT-EC-ISOGENY-WEIL
    • Needs MT-X0-HECKE
    • Needs MT-X0-CUSPS, MT-X0-EISENSTEIN-ALGEBRA, MT-NERON-SPECIALIZATION, MT-FFGS-OORT-RAYNAUD
    • Needs MT-BASE-INTEGRATED
  5. Mazur's prime-order argument
    • Needs MT-NERON-SPECIALIZATION, MT-FFGS-OORT-RAYNAUD
    • Needs MT-PRIME-SEMISTABLE
    • Needs MT-PRIME-OUTSIDE-IDENTITY, MT-X0-EISENSTEIN-QUOTIENT
    • Needs MT-PRIME-EISENSTEIN-SPECIALIZATION, MT-CYCLOTOMIC-UNRAMIFIED
    • Needs MT-PRIME-DIVISION-FIELD
    • Needs MT-PRIME-HERBRAND-KUMMER, MT-EC-ISOGENY-WEIL
    • Needs MT-TC-E1-JACOBIAN-VARIETY, MT-EC-ISOGENY-WEIL
    • Needs MT-PRIME-SPLIT-SEQUENCE, MT-PRIME-SHAFAREVICH
  6. Integration and hardening
    • Needs MT-BASE-INTEGRATED
    • Needs MT-FINITE-JOIN, MT-PRIME-ISOGENY-CHAIN, MT-PIN-MIGRATION
    • Needs MT-API-INTEGRATION
    • Needs MT-FINAL-ASSEMBLY

Prefer a theorem-first view? The canonical Verso blueprint includes proof-status summaries and its own interactive dependency graph. Open the formal blueprint

Critical dependency frontier

The shared infrastructure that gates Mazur’s argument.

These are coordination problems, not isolated bounties. Their interfaces should be owned centrally while proofs and vertical slices are distributed.

Extreme risk45 pts

MT-TC-D2-PICARD-REPRESENTABILITY

Representability and properness of Pic^0

Represent the degree-zero Picard functor and prove the resulting group scheme is proper and geometrically connected.

Tauceti
Needs
Unlocks
Extreme risk40 pts

MT-NERON-BASE

Neron models over discrete valuation rings

Construct Neron models with generic-fibre recovery and the Neron mapping property.

Mixed
Needs
Unlocks
Extreme risk40 pts

MT-FFGS-OORT-RAYNAUD

Oort-Tate classification and Raynaud uniqueness

Formalize the finite-flat classification and uniqueness results used to control prime-order subgroup schemes.

Mixed
Needs
Unlocks
Extreme risk40 pts

MT-X0-EISENSTEIN-QUOTIENT

Arithmetic of the Eisenstein quotient

Construct the Eisenstein quotient and prove finite Mordell-Weil group, exact cusp-difference order, and nonvanishing.

Mixed
Needs
Unlocks
Extreme risk35 pts

MT-TC-B1-COHERENT-COHOMOLOGY

Coherent cohomology of proper curves

Build finite-dimensional coherent cohomology on proper curves, including affine acyclicity and vanishing above degree one.

Tauceti
Needs
Unlocks
Extreme risk35 pts

MT-TC-D1-PICARD-FUNCTOR

Rigidified relative Picard functor

Define the fppf Picard sheaf, its degree-zero subfunctor, rigidification, and Poincare line bundle.

Tauceti
Needs
Unlocks

Open contracts

Exact Lean interfaces for proof and research.

Every card is an acceptance contract. There are 4 ordinary claims worth 39 points and 4 nonexclusive research intentions worth 74 points.

8challenges
OpenHigh risk

MT-X11-COSET · 12 points

The five-coset bound on X_1(11)

Every rational point on y^2 + y = x^3 - x^2 differs from one of the five multiples of (0,0) by five times a rational point.

MazurCompiled
Estimated proof
1,000–3,000 Lean lines
Suggested route
Complete the Kummer/Selmer calculation around the explicit five-isogeny and Miller function already recorded in XOneElevenDescent.
Skills
elliptic curves · isogeny descent · algebraic number theory
Claim this challengeView source
Lean acceptance boundaryChallenge.XOneElevenCoset
DeclarationMazurTheorem.Challenge.xOneEleven_fiveCosetBound
theorem xOneEleven_fiveCosetBound :
    MazurTorsion.XOneEleven.FiveCosetBound := sorry

Imports

  • MazurTorsion.NumberTheory.XOneElevenDescent

Consumed by

  • MazurTorsion.XOneEleven.five_point_classification_of_cosetBound

Destination

  • MazurTorsion.NumberTheory.XOneElevenDescent
  • MazurTorsion.XOneEleven.fiveCosetBound
Depends on
Unlocks
Research OpenExtreme risk

MT-X13-NONCUSP · 26 points

Classify the noncuspidal rational points on X_1(13)

The explicit X_1(13) sextic has no rational affine point away from the cusp abscissas 0 and -1.

MazurCompiled
Estimated proof
3,000–12,000 Lean lines
Suggested route
Use the prepared Pell certificate and a genus-two Jacobian or descent argument, or supply another kernel-checked rational-point classification.
Skills
genus-two curves · Jacobians · descent

Parallel approaches are welcome for this research-open boundary.

Register an approachView source
Lean acceptance boundaryChallenge.XOneThirteenNoncusp
DeclarationMazurTheorem.Challenge.xOneThirteen_no_noncuspidal_point
theorem xOneThirteen_no_noncuspidal_point
    (x y : ℚ) (hx0 : x ≠ 0) (hxnegOne : x ≠ -1)
    (hcurve : y ^ 2 =
      MazurTorsion.Kubert.orderThirteenHyperellipticPolynomial x) :
    False := sorry

Imports

  • MazurTorsion.NumberTheory.XOneThirteenDescent

Consumed by

  • MazurTorsion.rationalTorsion_orders_mem_cyclicOrders_of_remaining_obstructions

Destination

  • MazurTorsion.NumberTheory.XOneThirteenDescent
  • MazurTorsion.XOneThirteenDescent.no_noncuspidal_point
Depends on
Unlocks
Research OpenExtreme risk

MT-X18-NONCUSP · 18 points

Classify the noncuspidal rational points on the order-18 curve

If y^2 equals the explicit order-18 sextic at a rational x, then x is 0 or 1.

MazurCompiled
Estimated proof
2,000–5,000 Lean lines
Suggested route
Finish the classical Eisenstein π=3+ω descent using the primitive descent data already proved, or give another kernel-checked rational-point classification.
Skills
genus-two curves · descent · Eisenstein integers

Parallel approaches are welcome for this research-open boundary.

Register an approachView source
Lean acceptance boundaryChallenge.XOneEighteenNoncusp
DeclarationMazurTheorem.Challenge.xOneEighteen_no_noncuspidal_point
theorem xOneEighteen_no_noncuspidal_point
    (x y : ℚ) (hx0 : x ≠ 0) (hx1 : x ≠ 1)
    (hcurve : y ^ 2 =
      MazurTorsion.Kubert.orderEighteenHyperellipticPolynomial x) :
    False := sorry

Imports

  • MazurTorsion.NumberTheory.XOneEighteenDescent

Consumed by

  • MazurTorsion.rationalTorsion_orders_mem_cyclicOrders_of_remaining_obstructions

Destination

  • MazurTorsion.NumberTheory.XOneEighteenDescent
  • MazurTorsion.XOneEighteenDescent.no_noncuspidal_point
Depends on
Unlocks
Research OpenExtreme risk

MT-O25-EXCLUDE · 16 points

Exclude exact rational order 25

An elliptic curve over Q has no rational point of exact order 25.

MathlibCompiled
Estimated proof
2,000–7,000 Lean lines
Suggested route
Develop a Tate-normal-form or modular-curve reduction with an independently checkable descent endpoint.
Skills
elliptic curves · Tate normal form · explicit Diophantine geometry

Parallel approaches are welcome for this research-open boundary.

Register an approachView source
Lean acceptance boundaryChallenge.OrderTwentyFive
DeclarationMazurTheorem.Challenge.no_rational_point_of_order_twentyFive
theorem no_rational_point_of_order_twentyFive
    (E : WeierstrassCurve ℚ) [E.IsElliptic]
    (P : (E⁄ℚ).Point) :
    addOrderOf P ≠ 25 := sorry

Imports

  • MazurTorsion.Kubert.OrderTwentyFive

Consumed by

  • MazurTorsion.rationalTorsion_orders_mem_cyclicOrders_of_remaining_obstructions

Destination

  • MazurTorsion.Kubert.OrderTwentyFive
  • MazurTorsion.Kubert.rationalPoint_addOrderOf_ne_twentyFive
Depends on
Unlocks
Research OpenExtreme risk

MT-O35-EXCLUDE · 14 points

Exclude exact rational order 35

An elliptic curve over Q has no rational point of exact order 35.

MathlibCompiled
Estimated proof
2,000–7,000 Lean lines
Suggested route
Reduce to explicit compatible 5- and 7-isogeny data and close the resulting modular or Diophantine endpoint.
Skills
elliptic curves · isogenies · modular curves

Parallel approaches are welcome for this research-open boundary.

Register an approachView source
Lean acceptance boundaryChallenge.OrderThirtyFive
DeclarationMazurTheorem.Challenge.no_rational_point_of_order_thirtyFive
theorem no_rational_point_of_order_thirtyFive
    (E : WeierstrassCurve ℚ) [E.IsElliptic]
    (P : (E⁄ℚ).Point) :
    addOrderOf P ≠ 35 := sorry

Imports

  • MazurTorsion.Kubert.OrderThirtyFive

Consumed by

  • MazurTorsion.rationalTorsion_orders_mem_cyclicOrders_of_remaining_obstructions

Destination

  • MazurTorsion.Kubert.OrderThirtyFive
  • MazurTorsion.Kubert.rationalPoint_addOrderOf_ne_thirtyFive
Depends on
Unlocks
OpenHigh risk

MT-O49-TOWER · 10 points

Bridge exact order 49 to the X_0(49) correspondence

An elliptic curve over Q has no rational point of exact order 49.

MazurCompiled
Estimated proof
1,000–3,000 Lean lines
Suggested route
Use the compiled orderSevenG7F, exists_orderSevenHauptmodul_of_exactOrder, orderSevenQuotient, and orderSevenPointMap APIs; prove that the explicit Vélu point function respects addition or multiplication by seven; then carry an exact order-49 point through the nonbacktracking branch and apply XZeroFortyNine.no_noncuspidal_correspondence_point.
Skills
elliptic curves · Velu isogenies · explicit modular curves
Claim this challengeView source
Lean acceptance boundaryChallenge.OrderFortyNine
DeclarationMazurTheorem.Challenge.no_rational_point_of_order_fortyNine
theorem no_rational_point_of_order_fortyNine
    (E : WeierstrassCurve ℚ) [E.IsElliptic]
    (P : (E⁄ℚ).Point) :
    addOrderOf P ≠ 49 := sorry

Imports

  • MazurTorsion.NumberTheory.XZeroFortyNineTransfer

Consumed by

  • MazurTorsion.rationalTorsion_orders_mem_cyclicOrders_of_remaining_obstructions

Destination

  • MazurTorsion.NumberTheory.XZeroFortyNineTransfer
  • MazurTorsion.XZeroFortyNine.rationalPoint_addOrderOf_ne_fortyNine
Depends on
Unlocks
OpenHigh risk

MT-TC-A1-ORDER-SUPPORT · 15 points

Finite support of orders of rational functions

A nonzero rational function on a Noetherian integral scheme has nonzero order at only finitely many codimension-one points.

TaucetiCompiled
Estimated proof
200–1,500 Lean lines
Suggested route
Prove the global finiteness theorem upstream in Tau Ceti, then use it to package the existing local order maps as an OrderSystem.
Skills
algebraic geometry · Noetherian schemes · orders of vanishing
Claim this challengeView source
Lean acceptance boundaryMazurTauCetiChallenge.PrincipalSupport
DeclarationMazurTauCetiChallenge.finite_support_orderAt
theorem finite_support_orderAt
    (X : Scheme.{u}) [IsIntegral X] [IsNoetherian X]
    (g : Additive X.functionFieldˣ) :
    (Function.support fun x : TauCeti.AlgebraicGeometry.CodimensionOnePoint X =>
      TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderAt x g).Finite := sorry

Imports

  • TauCeti.AlgebraicGeometry.WeilDivisor.Principal.Basic
  • TauCeti.AlgebraicGeometry.WeilDivisor.Scheme.Order

Consumed by

  • MazurTauCetiChallenge.orderSystem

Destination

  • TauCeti.AlgebraicGeometry.WeilDivisor.Scheme.Order
  • TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finite_support_orderAt
Depends on
Unlocks
OpenMedium risk

MT-TC-E0-PRODUCT-DIM · 2 points

Dimension of a product of abelian varieties

The dimension of A × B is dim A + dim B for abelian varieties over a field.

TaucetiCompiled
Estimated proof
100–800 Lean lines
Suggested route
Reduce Tau Ceti's topological Krull dimension of the product scheme to the corresponding scheme-theoretic product-dimension theorem.
Skills
abelian varieties · Krull dimension · scheme products
Claim this challengeView source
Lean acceptance boundaryMazurTauCetiChallenge.ProductDimension
DeclarationMazurTauCetiChallenge.prod_dim
theorem prod_dim {K : Type u} [Field K]
    (A B : AbelianVariety K) :
    (AbelianVariety.prod A B).dim = A.dim + B.dim := sorry

Imports

  • TauCeti.AlgebraicGeometry.AbelianVariety.Product

Consumed by

  • MazurTauCetiChallenge.prod_self_dim

Destination

  • TauCeti.AlgebraicGeometry.AbelianVariety.Product
  • TauCeti.AlgebraicGeometry.AbelianVariety.prod_dim
Depends on
Unlocks

How progress is scored

Four gates. One weighted ledger.

A node earns no theorem-progress credit for a statement alone. A proof node earns 70% for an isolated kernel proof, 85% after API review, and 100% only after a downstream consumer compiles. Infrastructure earns 40% when its definitions compile, 70% after mathematical sanity checks, and 100% after a real downstream consumer compiles. The headline is the weighted sum.

  1. 01
    Statement

    The formal declaration faithfully matches the mathematics.

  2. 02
    Kernel proof

    Lean accepts it without project-specific axioms or placeholders.

  3. 03
    API accepted

    Definitions pass mathematical sanity checks and review.

  4. 04
    Integrated

    A named downstream consumer compiles against the result.

What 5% does—and does not—mean

It is an effort-weighted planning estimate, not a theorem of project management. The denominator is uncertain because Jacobians, integral modular curves, Néron models, and the Eisenstein quotient do not yet share a tested Lean spine.

The ≈12% ecosystem-ready figure is deliberately shown separately. It counts work that may be reusable from Lean Pool, Tau Ceti, FLT, and other audited repositories, but it earns integrated credit only after porting and consumer tests. Percentages will move as interfaces reveal the real work.

Inspect the ledger Read the methodology

Join the programme

Pick a boundary. Prove it. Connect it.

Contributors get an exact declaration, pinned dependencies, a named consumer, and review criteria. Maintainers coordinate the shared architecture so independent work composes.

Contribution guide Discuss an issue