Test Project · Local AI Infrastructure · Berlin · May 2026
p-adic Theory and Condensed Mathematics: a Test Project in Three Parts
Three interconnected sub-projects with a common mathematical background: formal verification in Lean 4 (condensed modules), classification-theoretic analysis (Dieudonné–Manin), and computer-algebraic experiments (formal groups).
Lean 4.31.0-rc2 + Mathlib · PARI/GP 2.17.3 · Hecke.jl / Julia 1.12 · Singular · deepseek-r1:70b · qwen3:235b-a22b · Mac Studio M3 Ultra (256 GB) · Stand: Juni 2026
Connection Between the Three Sub-projects
Sub-project 3 provides the concrete intuition: one can see, at an explicit elliptic curve, how formal groups over ℤp become isocrystals. Sub-project 2 classifies these isocrystals abstractly. Sub-project 1 formalises the condensed foundation into which both embed — p-divisible groups (generalising formal groups) are natural objects in the condensed world of Clausen–Scholze.
| Sub-project 3 | Sub-project 2 | Sub-project 1 |
|---|
Formal Groups
(PARI · Hecke · Singular) | Dieudonné–Manin
Classification | Solid Modules
(Lean 4 · Mathlib) |
| Concrete computation → | Abstract classification → | Formal foundation |
Sub-project 1 — Solid Condensed Modules: Formal Verification in Lean 4
Starting point
In Mathlib/Condensed/Solid.lean, lines 24–25, stood:
TODO (hard): prove that ((profiniteSolid ℤ).obj S).IsSolid for S : Profinite.
A condensed R-module is called solid when for every profinite set X the solidification morphism induces an isomorphism on Hom-sets: sol_X* : Hom(solid X, M) → Hom(free X, M) is an isomorphism. The functor profiniteSolid R is the right Kan extension of finFree R along FintypeCat.toProfinite. The mathematical argument was known (Clausen–Scholze, Prop. 5.7 in [CS19]); the Lean proof was missing.
File architecture
P0_SolLeftCancel_Axiom.lean — 1 Axiom
P1_Solid.lean — 0 Sorries
P2_finFree_Solid.lean — 0 Sorries (core)
P4_Solid_Progress.lean — 0 Sorries (wrapper)
Dependencies: P2 imports P0 + P1. P4 imports P2. No circular imports.
Complete lemma list
In P1_Solid.lean:
profiniteSolidCounit_isIso — the counit is an isomorphism at every T : FintypeCatprofiniteSolidification_comp_counit — sol_X ˆ counit_T = id (naturality equation)profiniteSolidification_isIso_at_fintype — the solidification morphism is iso at LTprofiniteSolid_isSolid_at_fintype — IsSolid when tested against images of FintypeCat
In P2_finFree_Solid.lean:
isSolid_of_isLimit_gen — a cofiltered limit of solid objects is solidfinFree_iso_solid — isomorphism solid(LT) ≅ finFree T for T : FintypeCatsurj_factor — surjectivity factorisation (core proof of the surjectivity half)surjectivity_from_surj_factor — lifting theorem from the factorisationfinFree_isSolid — IsSolid(finFree T) for T : FintypeCatprofiniteSolid_obj_isSolid_full — IsSolid(solid S) for all S : Profinite ← main result
Main result and proof structure
theorem profiniteSolid_obj_isSolid_full (S : Profinite.{u}) :
((profiniteSolid R).obj S).IsSolid
- profiniteSolidIsPointwiseRightKanExtension R: solid(S) is the limit limj finFree(Sj) over all finite quotients Sj of S (right Kan extension).
- isSolid_of_isLimit_gen: A cofiltered limit of solid objects is solid. Reduces the main result to: every finFree(Sj) is solid.
- finFree_isSolid: finFree T is solid for all T : FintypeCat. Follows from profiniteSolid_fintype_isSolid.
- IsSolid condition: The condition requires that (sol_X ˆ ·) : Hom(solidX, finFree T) → Hom(freeX, finFree T) is a bijection. Surjectivity: surjectivity_from_surj_factor (fully proved). Injectivity: Axiom sol_leftCancel.
Surjectivity — independent proof
The surjectivity of (sol_X ˆ ·) was proved independently of the axiom, via isColimitLocallyConstantPresheafDiagram: given h : freeX → finFree T, there exists (U0, q0, h0) with h = (profiniteFree R).map q0 ˆ h0. Set g = πU0,q0 ˆ h0. Then: sol_X ˆ g = h ✓. Surjectivity was thus formally complete.
Injectivity — the open problem and the axiom
Injectivity of (sol_X ˆ ·) requires that Hom(solid X, finFree T) = colimj Hom(finFree Xj, finFree T). This holds precisely when finFree T is a compact (tiny) object in CondensedMod R, i.e. when Hom(−, finFree T) commutes with cofiltered limits.
axiom sol_leftCancel (R : Type (u + 1)) [Ring R]
(T : FintypeCat.{u}) (X : Profinite.{u})
(f g : (profiniteSolid R).obj X ⟶ (finFree R).obj T)
(h : (profiniteSolidification R).app X ≫ f
= (profiniteSolidification R).app X ≫ g) : f = g
The axiom corresponds exactly to the injectivity of sol_X*, which follows from the Hom chain. It is mathematically correct (Clausen–Scholze, §5), but not formalisable in Lean because the required lemma (“discrete condensed modules are tiny”) does not exist in Mathlib and would require a standalone Mathlib contribution of approximately 200–400 lines of new Lean theory.
Exhaustively tested injectivity approaches (all failed)
- sol_X is epi in CondensedMod — false: {Σa∈X_j e_a}j does not lie in the image of sol_X for X = Cantor set
- hom_ext_of_isRightKanExtension — valid only for natural transformations between functors, not for individual morphisms
- IsLimit uniqueness (UMP) — gives uniqueness for morphisms to solid X, not from solid X
- LocallyConstant adjunction (LC ⊢ underlying) — wrong direction
- discreteUnderlyingAdj — gives Hom(discrete V, M), not Hom(M, discrete V)
#print axioms profiniteSolid_obj_isSolid_full (MathProject/P2_finFree_Solid.lean)
-- Axioms:
-- propext (Lean standard)
-- Classical.choice (Lean standard)
-- Quot.sound (Lean standard)
-- CondensedMod.sol_leftCancel ← only project-specific axiom (surj_factor is fully proved in P2)
MathProject build status (P0–P4): All 4 files build successfully. 0 sorries in any file.
PR branch (Mathlib/Condensed/Solid.lean): Latest commit 5874e87ae1 · CI Build ✅ · Lint style ✅ · 0 sorries · 2 axioms: sol_leftCancel + surj_factor (see below).
Lean 4.31.0-rc2. PR #39701 on leanprover-community/mathlib4.
Note on axiom vs. sorry: An axiom entry in Lean 4 is not a gap in the sense of a sorry, but an explicit, named and documented assumption. #print axioms shows it transparently. For a Mathlib PR, a project-specific axiom is not acceptable — the TODO thus remains open, supplemented by the proof infrastructure elaborated here.
Build status
All 4 MathProject .lean files build successfully with lake build (Lean 4.31.0-rc2 + Mathlib). 0 sorry in any file. In the MathProject, sol_leftCancel is the only project-specific axiom; surj_factor is fully proved. In Mathlib/Condensed/Solid.lean (PR branch), both sol_leftCancel and surj_factor are declared as axiom because the required colimit infrastructure (finFree_isColimit_at) and the CondensedMod ↔ TopMod equivalence are not yet in Mathlib. #print axioms shows them transparently; for a full Mathlib PR both axioms must be eliminated.
Why the axiom is not formalisable
The step “discrete condensed modules are tiny” requires the following Lean lemma, which does not exist in Mathlib:
theorem isDiscrete_isTiny (M : CondensedMod R) (hM : M.IsDiscrete)
{F : J ⊥ CondensedMod R} (c : Cone F) (hc : IsLimit c) :
Hom(c.pt, M) ≅ colim_j Hom(F.obj j, M)
This is a special case of the equivalence CondensedMod ↔ TopMod (topological R-modules), which is not formalised. For a future fully formal proof this gap must be closed first.
Sub-project 2 — Dieudonné–Manin Classification for All Dimensions
Starting point
Mathlib contains the Dieudonné–Manin theorem for dimension n = 1 in Mathlib/RingTheory/WittVector/Isocrystal.lean: a one-dimensional isocrystal over an algebraically closed field k of characteristic p is classified by a rational number m/n (the slope). The general theorem was missing.
Achieved: complete analysis and proof architecture
Using deepseek-r1:70b as analysis tool, the Lean infrastructure was mapped and a proof architecture for the general theorem elaborated. This sub-project was conceived as analysis and formalisation roadmap, not as Lean implementation.
Present in Mathlib: Definition of isocrystals as free W(k)-modules with Frobenius semi-linearity; simple isocrystals E(λ) for every rational slope λ ∈ ℚ; classification theorem for n = 1: fully proved; Witt vector infrastructure: Frobenius, Verschiebung, Teichmüller lift.
Elaborated proof architecture:
Step 1: Reduction to the irreducible case via slope filtration of the isocrystal. Lean precedents in Witt vector infrastructure available.
Step 2: Reduction to the simple case — every irreducible summand ≅ E(m/n) via tensor product argument from the n=1 case.
Step 3: Uniqueness of the decomposition E(m1/n1) ⊕ ··· ⊕ E(mr/nr). The multiplicities are uniquely determined by the slope filtration.
Missing for a Lean implementation: Formal decomposition lemma into irreducible summands (no Lean proof); uniqueness theorem in Lean; complete slope filtration as Lean theorem.
Mathematical relevance: The general Dieudonné–Manin theorem classifies exactly the objects that Sub-project 3 constructs computationally. It touches Witt vectors, Frobenius semi-linearity and crystalline cohomology and is a direct foundation for p-adic representation theory and the Langlands programme.
Sub-project 3 — Formal Groups over ℤp: Computer-Algebraic Experiment
Curve and starting point
Elliptic curve E: y² = x³ − x over ℤ. j-invariant 1728, torsion group ℤ/2 × ℤ/2, analytic rank 0, complex multiplication by ℤ[i]. Three systems were used: PARI/GP for the formal law, Hecke.jl for point counts and ap, Singular for the algebraic structure mod p.
Results with PARI/GP
Formal group law (to degree 5):
F(X,Y) = X + Y + 2XY² + 2X²Y − X⁴Y − XY⁴ + O(degree 6)
Formal logarithm (to degree 22, all coefficients exact):
L(t) = t − (2/5)t⁵ + (2/3)t⁹ − (20/13)t¹³ + (70/17)t¹⁷ − 12t²¹ + O(t²³)
Multiplication series [n](t) = L&supmin;¹(n·L(t)):
[3](t) = 3T + 96T⁵ + 2432T⁹ + 62976T¹³ + 1628160T¹⁷ + ...
[5](t) = 5T + 1248T⁵ + 257920T⁹ + 54156800T¹³ + ...
Height determination (first non-vanishing term mod p in [p](t)):
| p | First term mod p | Height | Type | Isocrystal (Sub-project 2) |
|---|
| 3 | 2·T&sup9; | h = 2 | supersingular (a3 = 0) | E(1/2), slope = 1/2 |
| 5 | 3·T&sup5; | h = 1 | ordinary (a5 = −2 ≠ 0) | E(0/1), slope = 0 |
Results with Hecke.jl (ap and |E(𝔽p)| for all primes to 43)
| p | |E(𝔽p)| | ap | Type | p mod 4 |
|---|
| 3 | 4 | 0 | supersingular | 3 |
| 5 | 8 | −2 | ordinary | 1 |
| 7 | 8 | 0 | supersingular | 3 |
| 11 | 12 | 0 | supersingular | 3 |
| 13 | 8 or 6 | ±6 or ±2 | ordinary | 1 |
| 43 | 44 | 0 | supersingular | 3 |
CM structure: Supersingular reduction occurs precisely at p ≡ 3 (mod 4) — E has complex multiplication by ℤ[i], and i has norm p precisely when p ≡ 1 (mod 4). The pattern is directly and completely readable in the ap table.
Results with Singular
F mod 3 = −t₁⁴t₂ − t₁t₂⁴ − t₁³t₂ + t₁²t₂² − t₁t₂³ − t₁²t₂ − t₁t₂² + t₁ + t₂
F mod 5 = −t₁⁴t₂ + 2t₁³t₂² + 2t₁²t₂³ − t₁t₂⁴ − t₁³t₂ − 2t₁²t₂² − t₁t₂³ − t₁²t₂ − t₁t₂² + t₁ + t₂
The print(string, poly) command failed with a syntax error (GP compatibility issue); the jet() call for [p](t) mod p yielded the correct low-degree terms.
Connection to Sub-project 2
The isocrystal of the formal group Êp at prime p is precisely the object that Sub-project 2 classifies: height h = 1 → slope 0 → E(0/1); height h = 2 → slope 1/2 → E(1/2). The computations make the abstract classification visible at a concrete example.
Overall Assessment
| Sub-project | Type | Outcome |
|---|
| 1 — Solid Modules (Lean 4) | Formal verification | 8 theorems proved in Solid.lean · 0 sorries · 2 axioms: sol_leftCancel (injectivity) + surj_factor (surjectivity, proved in MathProject/P2) · CI Build ✅ Lint ✅ · commit 5874e87ae1 · Lean 4.31.0-rc2 · PR #39701 on leanprover-community/mathlib4 |
| 2 — Dieudonné–Manin | Analysis and proof architecture | Mathlib status mapped · three-step proof architecture elaborated · missing Lean lemmas precisely identified |
| 3 — Formal Groups | Computer-algebraic experiment | F(X,Y) to degree 5 · L(t) to degree 22 · [3](t) and [5](t) · heights h=2/h=1 · ap to 43 · CM structure confirmed · Singular representations mod 3 and mod 5 |
Philosophical aspects: None of the three sub-projects had an independent philosophical research question. The mathematical background — condensed mathematics as a new foundation of analysis and algebra (Clausen–Scholze), the classification by slopes as an ordering principle in p-adic Hodge theory — has philosophical dimensions that were not, however, the subject of this project.
T. Riepe, Berlin. May 2026 (updated June 2026). GitHub: thothrde/mathlib4 · MathProject/ · PR #39701 on leanprover-community/mathlib4. Lean 4.31.0-rc2. CI Build ✅ Lint ✅. Condensed mathematics after Clausen–Scholze [CS19]. Dieudonné–Manin after Katz (1979).
Testprojekt · Lokale KI-Infrastruktur · Berlin · Mai 2026
p-adische Theorie und kondensierte Mathematik:
ein Testprojekt in drei Teilen
Drei zusammenhängende Teilprojekte mit gemeinsamem mathematischem Hintergrund: formale Verifikation in Lean 4 (kondensierte Moduln), klassifikationstheoretische Analyse (Dieudonné-Manin) und computeralgebraisches Experiment (formale Gruppen). Die Werkzeuge: Lean 4 + Mathlib, PARI/GP, Hecke.jl, Singular, deepseek-r1:70b.
Lean 4.31.0-rc2 + Mathlib · PARI/GP 2.17.3 · Hecke.jl / Julia 1.12 · Singular · deepseek-r1:70b · qwen3:235b-a22b · Mac Studio M3 Ultra (256 GB) · Stand: Juni 2026
Zusammenhang der drei Teilprojekte
Teilprojekt 3 liefert die konkrete Anschauung: Man sieht an einer expliziten elliptischen Kurve, wie formale Gruppen über ℤ_p zu Isocrystallen werden. Teilprojekt 2 klassifiziert diese Isocrystalle abstrakt. Teilprojekt 1 formalisiert das kondensierte Fundament, in das beides einbettet — p-divisible Gruppen (die formale Gruppen verallgemeinern) sind natürliche Objekte in der kondensierten Welt von Clausen-Scholze.
Teilprojekt 3Formale Gruppen
PARI · Hecke · Singular
→
Teilprojekt 2Dieudonné-Manin
Klassifikation
→
Teilprojekt 1Solid Modules
Lean 4 · Mathlib
Teilprojekt 1
Solid kondensierte Moduln — formale Verifikation in Lean 4
Ausgangspunkt
In Mathlib/Condensed/Solid.lean, Zeilen 24–25, stand:
TODO (hard): prove that ((profiniteSolid ℤ).obj S).IsSolid for S : Profinite.
Ein kondensierter R-Modul heißt solid, wenn für jede profinite Menge X der Solidifizierungsmorphismus einen Isomorphismus auf Hom-Mengen induziert:
sol_X* : Hom(solid X, M) → Hom(free X, M) ist ein Isomorphismus
Der Funktor profiniteSolid R ist die rechtsseitige Kan-Erweiterung von finFree R entlang FintypeCat.toProfinite. Die Frage: Ist solid(S) selbst solid? Das mathematische Argument war bekannt (Clausen-Scholze, Prop. 5.7 in [CS19]), der Lean-Beweis fehlte.
Datei-Architektur
P0_SolLeftCancel
_Axiom.lean
1 Axiom
P2_finFree
_Solid.lean
0 Sorries (Kern)
P4_Solid
_Progress.lean
0 Sorries (Wrapper)
Abhängigkeiten: P2 importiert P0 + P1. P4 importiert P2. Kein Kreisimport.
Alle Lean-Dateien und ihre Inhalte
| Datei | Inhalt | Status | GitHub |
|---|
P0_SolLeftCancel_Axiom.lean | Axiom sol_leftCancel mit vollständiger Dokumentation | 1 axiom | GitHub → |
P1_Solid.lean | Vier Iso-Lemmata, Koeinheit-Infrastruktur | 0 sorries | GitHub → |
P2_finFree_Solid.lean | Vollständige Beweiskette, Hauptresultat | 0 sorries | GitHub → |
P4_Solid_Progress.lean | Wrapper, Alias profiniteSolid_fintype_isSolid_v2 | 0 sorries | GitHub → |
Vollständige Lemma-Liste
In P1_Solid.lean:
profiniteSolidCounit_isIso — die Koeinheit ist an jedem T : FintypeCat ein IsomorphismusprofiniteSolidification_comp_counit — sol_X ≫ counit_T = id (Naturalitätsgleichung)profiniteSolidification_isIso_at_fintype — der Solidifizierungsmorphismus ist Iso bei LTprofiniteSolid_isSolid_at_fintype — IsSolid wenn gegen Bilder von FintypeCat getestet
In P2_finFree_Solid.lean:
isSolid_of_isLimit_gen — ein kofiltrierter Limes solid-Objekte ist solidfinFree_iso_solid — Isomorphismus solid(LT) ≅ finFree T für T : FintypeCatsol_map_counit — Naturalitätsgleichung für den Solidifizierungsmorphismusiso_counit_sol — Umkehrrichtung der KoeinheitsnaturalitätfinFree_isDiscrete — finFree T ist diskret in CondensedMod RfinFree_isColimit_at — (finFree T)(X) = colim_j (finFree T)(X_j)surj_factor — Surjektivitätsfaktorisierung (Kernbeweis der Surjektivitätshälfte)surjectivity_from_surj_factor — Lifting-Theorem aus der Faktorisierungsol_leftCancel_finite — Linkskancellation von sol bei endlichen QuotientenprofiniteSolid_fintype_isSolid — IsSolid(solid LT) für T : FintypeCatfinFree_isSolid — IsSolid(finFree T) für T : FintypeCatprofiniteSolid_obj_isSolid_full — IsSolid(solid S) für alle S : Profinite ← Hauptresultat
Zusätzlich in Mathlib/Condensed/Solid.lean (PR-Branch), ebenfalls sorry-frei:
profiniteSolidCounit_isIso, profiniteSolidification_isIso_at_fintype, finFreeIsoSolid, sol_map_counit, profiniteSolid_fintype_isSolid, isSolid_of_isLimit_gen, finFree_isSolid, profiniteSolid_obj_isSolid
Axiome in Solid.lean (PR-Branch): sol_leftCancel (Injektivität) + surj_factor (Surjektivitätsfaktorisierung; in MathProject/P2 vollständig bewiesen, aber finFree_isColimit_at-Infrastruktur noch nicht in Mathlib). CI: Build ✅ · Lint ✅ · Lean 4.31.0-rc2 · Commit 5874e87ae1.
Hauptresultat und Beweisstruktur
Hauptresultat
theorem profiniteSolid_obj_isSolid_full (S : Profinite.{u}) :
((profiniteSolid R).obj S).IsSolid
1
profiniteSolidIsPointwiseRightKanExtension R: solid(S) ist der Limes limj finFree(Sj) über alle endlichen Quotienten Sj von S (rechtsseitige Kan-Erweiterung).
2
isSolid_of_isLimit_gen: Ein kofiltrierter Limes solid-Objekte ist solid. Reduziert das Hauptresultat auf: jedes finFree(Sj) ist solid.
3
finFree_isSolid: finFree T ist solid für alle T : FintypeCat. Folgt aus profiniteSolid_fintype_isSolid.
4
solid(LT) ist solid: Die IsSolid-Bedingung verlangt, dass (sol_X ≫ ·) : Hom(solidX, finFree T) → Hom(freeX, finFree T) eine Bijektion ist. Surjektivität: surjectivity_from_surj_factor (vollständig bewiesen). Injektivität: Axiom sol_leftCancel.
Surjektivität — eigenständiger Beweis
Die Surjektivität von (sol_X ≫ ·) wurde unabhängig vom Axiom bewiesen, via isColimitLocallyConstantPresheafDiagram:
Hom(freeX, finFree T) = colim_{U: DQ(X)} Hom(finFree U, finFree T)
(Garben-Colimes-Eigenschaft, Mathlib: Condensed.Discrete.Colimit)
Gegeben h : freeX → finFree T:
∃ (U₀, q₀, h₀) mit h = (profiniteFree R).map q₀ ≫ h₀
Setze g = π_{U₀,q₀} ≫ h₀ (Limesprojektion auf finFree U₀, dann h₀)
Dann: sol_X ≫ g = h ✓
Die Surjektivität war somit formell vollständig. Das verbleibende Problem war ausschließlich die Injektivität.
Injektivität — das offene Problem und das Axiom
Die Injektivität von (sol_X ≫ ·) erfordert, dass Hom(solid X, finFree T) = colimj Hom(finFree Xj, finFree T). Dies gilt genau dann, wenn finFree T ein kompaktes Objekt (tiny object) in CondensedMod R ist, d.h. wenn Hom(−, finFree T) mit kofiltriert Limiten vertauscht.
Da finFree T diskret ist (bewiesen: finFree_isDiscrete), und diskrete kondensierte Moduln tiny sind, liefert die vollständige Hom-Kette:
Hom(solid X, finFree T)
= colim_j Hom(finFree X_j, finFree T) [finFree T ist tiny ← aus Diskretheit]
= colim_j (finFree T)(X_j) [free-forget Adjunktion + Yoneda ✓]
= (finFree T)(X) [finFree_isColimit_at ✓]
= Hom(free X, finFree T) [Adjunktion ✓]
Axiom — P0_SolLeftCancel_Axiom.lean
axiom sol_leftCancel (R : Type (u + 1)) [Ring R]
(T : FintypeCat.{u}) (X : Profinite.{u})
(f g : (profiniteSolid R).obj X ⟶ (finFree R).obj T)
(h : (profiniteSolidification R).app X ≫ f
= (profiniteSolidification R).app X ≫ g) : f = g
Das Axiom entspricht exakt der Injektivität von sol_X*, die aus der Hom-Kette folgt. Es ist mathematisch korrekt (Clausen-Scholze, §5), aber nicht in Lean formalisierbar.
Warum das Axiom nicht formalisierbar ist
Der Schritt „diskrete kondensierte Moduln sind tiny" benötigt das folgende Lean-Lemma, das in Mathlib nicht existiert:
theorem isDiscrete_isTiny (M : CondensedMod R) (hM : M.IsDiscrete)
{F : J ⥤ CondensedMod R} (c : Cone F) (hc : IsLimit c) :
Hom(c.pt, M) ≅ colim_j Hom(F.obj j, M)
Dieses ist ein Spezialfall der Äquivalenz CondensedMod ↔ TopMod (topologische R-Moduln), die nicht formalisiert ist. Für einen künftigen vollständigen Beweis wäre ein eigenständiger Mathlib-Beitrag von ca. 200–400 Zeilen neuer Lean-Theorie nötig, der zeigt, dass Morphismen in CondensedMod von profinit-erzeugten Moduln zu diskreten Moduln stetige Schnittabbildungen induzieren.
Außerdem fehlen in Mathlib:
- Die vollständige Äquivalenz CondensedMod ↔ TopMod
- Der analytische Beweis via Maßtheorie (Clausen-Scholze)
- Die topologische Stetigkeitscharakterisierung von Garben-Morphismen
Erschöpfend getestete Beweisansätze für Injektivität (alle gescheitert)
sol_X ist Epi in CondensedMod — falsch: Element {Σ_{a∈X_j} e_a}_j liegt für X = Cantor-Menge nicht im Bild von sol_X.
hom_ext_of_isRightKanExtension — gilt nur für natürliche Transformationen zwischen Funktoren, nicht für Einzelmorphismen.
IsLimit-Eindeutigkeit (UMP) — gibt Eindeutigkeit für Morphismen nach solid X, nicht von solid X.
LocallyConstant-Adjunktion (LC ⊣ underlying) — falsche Richtung; liefert Hom von LC-Objekten.
discreteUnderlyingAdj — liefert Hom(discrete V, M), nicht Hom(M, discrete V).
Surjektivität von (sol_X)_S an beliebigem Schnitt — falsch für unendliches X.
Schnitteigenschaft via Sektion-Level — Image von sol_X erzeugt lim_j R^{C(S,X_j)} nicht für unendliches S.
#print axioms
#print axioms profiniteSolid_obj_isSolid_full
-- Axioms:
-- propext (Lean-Standard)
-- Classical.choice (Lean-Standard)
-- Quot.sound (Lean-Standard)
-- CondensedMod.sol_leftCancel ← einziges projektspezifisches Axiom
Build-Status
| Lake-Build-Befehl | Jobs | Ergebnis |
|---|
lake build MathProject.P0_SolLeftCancel_Axiom | 2139 | ✓ erfolgreich |
lake build MathProject.P1_Solid | 2145 | ✓ erfolgreich |
lake build MathProject.P2_finFree_Solid | 2193 | ✓ + Axiom-Hinweis |
lake build MathProject.P4_Solid_Progress | 2194 | ✓ erfolgreich |
Lean 4.31.0-rc2, Mathlib 4, Mac Studio M3 Ultra 256 GB. Kein sorry in keiner Datei (MathProject P0–P4). #print axioms profiniteSolid_obj_isSolid_full (MathProject): einziges projektspezifisches Axiom CondensedMod.sol_leftCancel — surj_factor dort vollständig bewiesen.
PR-Branch (Mathlib/Condensed/Solid.lean): Letzter Commit 5874e87ae1 · CI Build ✅ · Lint style ✅ · 0 sorries · 2 Axiome: sol_leftCancel + surj_factor (Colimit-Infrastruktur noch nicht in Mathlib). PR #39701 auf leanprover-community/mathlib4.
Hinweis zu Axiom vs. sorry: Ein axiom-Eintrag in Lean 4 ist keine Lücke im Sinn eines sorry, sondern eine explizite, benannte und dokumentierte Annahme. #print axioms zeigt sie transparent. Für einen Mathlib-PR ist ein projektspezifisches Axiom nicht akzeptabel — das TODO bleibt dann weiterhin offen, ergänzt um die hier ausgearbeitete Beweis-Infrastruktur.
Teilprojekt 2
Dieudonné-Manin-Klassifikationssatz für alle Dimensionen
Ausgangspunkt
Mathlib enthält den Dieudonné-Manin-Satz für Dimension n = 1 in Mathlib/RingTheory/WittVector/Isocrystal.lean: ein eindimensionales Isocrystal über einem algebraisch abgeschlossenen Körper k der Charakteristik p ist durch eine rationale Zahl m/n (die Slope) klassifiziert. Der allgemeine Satz fehlte.
Erreicht: vollständige Analyse und Beweis-Architektur
Mit deepseek-r1:70b als Analysewerkzeug wurde die Lean-Infrastruktur kartiert und eine Beweis-Architektur für den allgemeinen Satz ausgearbeitet. Dieses Teilprojekt war als Analyse und Formalisierungs-Roadmap angelegt, nicht als Lean-Implementierung.
In Mathlib vorhanden:
- Definition von Isocrystallen als freie W(k)-Moduln mit Frobenius-Halblinearität
- Einfache Isocrystalle E(λ) für jede rationale Slope λ ∈ ℚ
- Klassifikationssatz für n = 1: vollständig bewiesen
- Witt-Vektor-Infrastruktur: Frobenius, Verschiebung, Teichmüller-Lift
Ausgearbeitete Beweis-Architektur
Schritt 1: Reduktion auf den irreduziblen Fall
über die Slope-Filtrierung des Isocrystalls.
Lean-Vorbilder in WittVector-Infrastruktur vorhanden.
Schritt 2: Reduktion auf den einfachen Fall
— jeder irreduzible Anteil ≅ E(m/n)
via Tensorprodukt-Argument aus dem n=1-Fall.
Schritt 3: Eindeutigkeit der Zerlegung
E(m₁/n₁) ⊕ ··· ⊕ E(mᵣ/nᵣ)
Die Multiplizitäten sind durch die Slope-Filtrierung
eindeutig bestimmt.
Fehlend für eine Lean-Implementierung:
- Formales Zerlegungslemma in irreduzible Summanden (kein Lean-Beweis)
- Eindeutigkeitssatz in Lean
- Vollständige Slope-Filtrierung als Lean-Theorem
Mathematische Relevanz
Der allgemeine Dieudonné-Manin-Satz klassifiziert genau die Objekte, die Teilprojekt 3 computational konstruiert. Er berührt Witt-Vektoren, Frobenius-Halblinearität und Kristallkohomologie und ist direktes Fundament für p-adische Darstellungstheorie und das Langlands-Programm.
Teilprojekt 3
Formale Gruppen über ℤ_p — computeralgebraisches Experiment
Kurve und Ausgangspunkt
Elliptische Kurve E: y² = x³ − x über ℤ. j-Invariante 1728, Torsionsgruppe ℤ/2 × ℤ/2, analytischer Rang 0, komplexe Multiplikation durch ℤ[i]. Drei Systeme wurden eingesetzt: PARI/GP für das Formalgesetz, Hecke.jl für Punktzahlen und a_p, Singular für die algebraische Struktur mod p.
Ergebnisse mit PARI/GP
Formales Gruppengesetz (bis Grad 5):
F(X,Y) = X + Y + 2XY² + 2X²Y − X⁴Y − XY⁴ + O(Grad 6)
Formaler Logarithmus (bis Grad 22, alle Koeffizienten exakt):
L(t) = t − (2/5)t⁵ + (2/3)t⁹ − (20/13)t¹³ + (70/17)t¹⁷ − 12t²¹ + O(t²³)
Multiplikationsreihen [n](t) = L⁻¹(n·L(t)):
[3](t) = 3T + 96T⁵ + 2432T⁹ + 62976T¹³ + 1628160T¹⁷ + ···
[5](t) = 5T + 1248T⁵ + 257920T⁹ + 54156800T¹³ + ···
Höhenbestimmung (erster nichtverschwindender Term mod p in [p](t)):
| p | Erster Term mod p | Höhe | Typ | Isocrystal (Teilprojekt 2) |
|---|
| 3 | 2·T⁹ | h = 2 | supersingulär (a₃ = 0) | E(1/2), Slope = 1/2 |
| 5 | 3·T⁵ | h = 1 | gewöhnlich (a₅ = −2 ≠ 0) | E(0/1), Slope = 0 |
Ergebnisse mit Hecke.jl
a_p und |E(𝔽_p)| für alle Primzahlen bis 43:
| p | |E(𝔽_p)| | a_p | Typ | p mod 4 |
|---|
| 3 | 4 | 0 | supersingulär | 3 |
| 5 | 8 | −2 | gewöhnlich | 1 |
| 7 | 8 | 0 | supersingulär | 3 |
| 11 | 12 | 0 | supersingulär | 3 |
| 13 | 8 | 6 | gewöhnlich | 1 |
| 17 | 16 | 2 | gewöhnlich | 1 |
| 19 | 20 | 0 | supersingulär | 3 |
| 23 | 24 | 0 | supersingulär | 3 |
| 29 | 40 | −10 | gewöhnlich | 1 |
| 31 | 32 | 0 | supersingulär | 3 |
| 37 | 40 | −2 | gewöhnlich | 1 |
| 41 | 32 | 10 | gewöhnlich | 1 |
| 43 | 44 | 0 | supersingulär | 3 |
CM-Struktur: Superinguläre Reduktion genau bei p ≡ 3 (mod 4) — E hat komplexe Multiplikation durch ℤ[i], und i hat Norm p genau wenn p ≡ 1 (mod 4). Das Muster ist in der a_p-Tabelle direkt und vollständig ablesbar. Hecke.jl zeigte einen MethodError für rank(), der die a_p-Berechnungen nicht beeinträchtigte.
Ergebnisse mit Singular
F mod 3 = −t₁⁴t₂ − t₁t₂⁴ − t₁³t₂ + t₁²t₂² − t₁t₂³ − t₁²t₂ − t₁t₂² + t₁ + t₂
F mod 5 = −t₁⁴t₂ + 2t₁³t₂² + 2t₁²t₂³ − t₁t₂⁴ − t₁³t₂ − 2t₁²t₂² − t₁t₂³ − t₁²t₂ − t₁t₂² + t₁ + t₂
Der print(string, poly)-Befehl schlug mit Syntaxfehler fehl (GP-Kompatibilitätsproblem); der jet()-Aufruf für [p](t) mod p lieferte die korrekten niedriggradigen Terme.
Verbindung zu Teilprojekt 2
Das Isocrystal der formalen Gruppe Ê_p bei der Primzahl p ist genau das Objekt, das Teilprojekt 2 klassifiziert: Höhe h = 1 → Slope 0 → E(0/1); Höhe h = 2 → Slope 1/2 → E(1/2). Die Berechnungen machen die abstrakte Klassifikation an einem konkreten Beispiel sichtbar.
Gesamtbilanz
| Teilprojekt | Art | Abschluss |
|---|
| 1 — Solid Modules (Lean 4) |
Formale Verifikation |
8 Theoreme in Solid.lean bewiesen · 0 sorries · 2 Axiome: sol_leftCancel (Injektivität) + surj_factor (Surjektivität, in MathProject/P2 bewiesen) · CI Build ✅ Lint ✅ · Commit 5874e87ae1 · Lean 4.31.0-rc2 · PR #39701 auf leanprover-community/mathlib4 |
| 2 — Dieudonné-Manin |
Analyse und Beweis-Architektur |
Mathlib-Stand kartiert · Drei-Schritte-Beweis-Architektur ausgearbeitet · fehlende Lean-Lemmata präzise identifiziert |
| 3 — Formale Gruppen |
Computeralgebraisches Experiment |
F(X,Y) bis Grad 5 · L(t) bis Grad 22 · [3](t) und [5](t) · Höhen h=2/h=1 · a_p bis 43 · CM-Struktur bestätigt · Singular-Darstellungen mod 3 und mod 5 |
Philosophische Aspekte: Keine der drei Teilprojekte hatte eine eigenständig philosophische Fragestellung. Der mathematische Hintergrund — kondensierte Mathematik als neue Grundlegung der Analysis und Algebra (Clausen-Scholze), die Klassifikation durch Slopes als Ordnungsprinzip in der p-adischen Hodge-Theorie — hat philosophische Dimensionen, die aber nicht Gegenstand dieses Projekts waren.