0
~115 distinct
Verified results
0 sorry · no custom axioms
0
%
Frontier mapped
486 corpus claims
0
claims
Foundations blocking
each = a research-grade gap
~10–15%
Honest substantive
rest = verified engineering
02Frontier map — 486 corpus claims
Every claim's status is fixed, reserved, and never guessed — see the table view for the exact rule behind each color.
verified 5 tractable 39 partial 32 blocked 148 informal 164 unassigned 98
Table view
| Status | Claims | Share | Meaning |
|---|---|---|---|
| verified | 5 | 1.0% | kernel-checked |
| tractable | 39 | 8.0% | reachable, no new foundation |
| partial | 32 | 6.6% | some progress possible |
| blocked | 148 | 30.5% | needs a missing foundation |
| informal | 164 | 33.7% | not a formal statement by nature |
| unassigned | 98 | 20.2% | not yet triaged |
Frontier completeness
every claim assigned a status + (if blocked) a named missing foundation
every claim assigned a status + (if blocked) a named missing foundation
03Blocked by missing foundation
semaev polynomials
51
cost model
35
curve depth
33
quantum cost
29
lattice reduction
25
weil pairing
8
point counting
0
Table view
| Foundation | Claims blocked | Leverage | Effort | Gap |
|---|---|---|---|---|
| semaev polynomials | 51 | medium | weeks-months | MvPolynomial exists but not the elliptic summation polynomials Sₙ (index calculus over extension fields). |
| cost model | 35 | medium | weeks-months | No group-operation / oracle-query cost model, so exact Θ running times (index calculus, distinguished points) can't be stated. The generic Ω(√p) core was formalized by sidestepping this. |
| curve depth | 33 | medium | weeks each rung | Mathlib has EllipticCurve + group law, but not the deeper ECDLP constructions (higher division polynomials, torsion structure E[n]≅(ℤ/n)², isogeny depth). Partly tractable — the active Track-B DAG. |
| quantum cost | 29 | low (out of scope) | n/a | No quantum circuit cost model (Shor-style resource estimates). Out of scope for Mathlib. |
| lattice reduction | 25 | medium | months | No LLL/BKZ/CVP. Blocks HNP / biased-nonce ECDSA attack formalizations. |
| weil pairing | 8 | highest | months (research-grade) | No Weil/Tate pairing eₙ. Needs divisors, function fields, Miller's algorithm. Gates the MOV/Frey-Rück transfer reduction itself. |
| point counting | 0 | high | months (research-grade) | No Schoof / point-counting; #E(𝔽_p)=n cannot be computed (native_decide can't enumerate 2^256 points). Gates the GLV [λ]-eigenvalue claim and the ℤ/n-module structure needed to instantiate the protocol algebra. |
04Environment layers
L1
Verified core
kernel-checked theorems (absolute trust)
kernel-checked theorems (absolute trust)
L2
Frontier map
what's open/blocked & by which missing foundation
what's open/blocked & by which missing foundation
L3
Navigable structure
machine-readable graph + queryable data
machine-readable graph + queryable data
L4
Formalized objects
GLV (cube-root + torsion-preserving), torsion, division polys
GLV (cube-root + torsion-preserving), torsion, division polys
L5
Engine
AI+kernel pipeline; self-extensible substrate
AI+kernel pipeline; self-extensible substrate
05Tracks & checkpoints
A — Frontier map (machine-actionable)
- A1 frontier_map.json + query
- A2 status+foundation for every claim (79.8%)
- A3 per-foundation unlock lists
B — Depth (verified foundations, DAG)
- GLV object: equation→hom→cube-root→torsion-preserving
- E[n] group object bridged
- next rung → E[n]≅(ℤ/n)² (blocked by point-counting)
C — Engine & extensibility
- CI trust gates (no-sorry, axiom audit, count/import)
- generator + prover loop
- warm server node (idle — needs PAT)
06Recent build milestones
a25f657Merge #30: torsion tower + GLV End(E) structure + dashboard/logoecff012Prove uniform odd-torsion bound: #E[n] <= n^2 for all odd n coprime to pc4ad13aProve secp256k1 5-torsion structure via the 5-division polynomial31e18f0Consolidate the GLV formalization into a citable writeup78f8cd6Add Manus task brief: provision + run the Layer-2 prover node564ee5dProve GLV endomorphism is an order-3 automorphism of the point group8c00793Prove GLV endomorphism satisfies its minimal polynomial in End(E)8bd492dUse the exact deck keyAI wordmark as the site logo53b8491Rebuild logo as key-glyph mark; fix KPI stat-tile row; add scroll-progress bar920ac07Major dashboard redesign: real logo, sticky scrollspy nav, dataviz-method charts, a11yec2703aRebrand dashboard to match the KeyAI deck: navy/blue palette, Baloo 2 + Nunito (self-hosted), card style4dd9ef2Redesign main page: full auto-discovered navigation hub (44 links, 6 sections, no dead/missing entries)7d93f9bPages: also emit index.html so the site root shows the dashboard3bf4f22Observation interface: scripts/build_dashboard.py + dashboard.html (metrics, layers, tracks, frontier, milestones)