# formalization.yaml (v0.3): repo-root metadata for formalization projects. # Schema: https://github.com/mathlib-initiative/formalization.yaml version: "v0.3" project: name: "jordan_pick — Pick's theorem + the Jordan curve theorem (Lean 4 / Mathlib)" authors: - "Rado Kirov" # human director; the formalization itself is agent-produced — see `automation` license: "Apache-2.0" sources: - title: "lean-eval Pick problem (LeanEval/Geometry/PicksTheorem.lean)" authors: ["Lean FRO (leanprover/lean-eval)"] id: "https://lean-lang.org/eval/problems/pick/ — the exact target statement, proved verbatim in EvalBridgeMain.lean" type: "specification / eval problem" license: "Apache-2.0" author_contacted: "no" prior_work: "" - title: "lean-eval Jordan curve problem (jordan_curve)" authors: ["Lean FRO (leanprover/lean-eval)"] id: "https://lean-lang.org/eval/problems/jordan_curve/ — the exact target statement, proved verbatim in JordanPick/JordanCurve.lean" type: "specification / eval problem" license: "Apache-2.0" author_contacted: "no" prior_work: "" - title: "lean-eval Radó theorem problem (rado_riemannSurface)" authors: ["Junyan Xu (submitter); Lean FRO (leanprover/lean-eval)"] id: "https://lean-lang.org/eval/problems/rado_riemannSurface/ — the exact target statement, proved verbatim in Rado/Main.lean" type: "specification / eval problem" license: "Apache-2.0" author_contacted: "no" prior_work: > Two prior automated solutions are recorded on the leaderboard (Aristotle/Harmonic 2026-06-22, Seed Prover/ByteDance 2026-06-28); both submission repos are private and neither proof was seen. Clean-room: this development was produced independently from the mathematical literature below. This submission passed the lean-eval comparator (2026-07-10). - title: "A short proof of the uniformization theorem (self-contained Perron/Radó treatment)" authors: ["Cipriana Anghel", "Rareş Stan"] id: "arXiv:2008.12189; Ann. Glob. Anal. Geom. (2022)" type: "paper (primary mathematical source for the Radó development)" license: "" author_contacted: "no" prior_work: > Informal mathematics only (no prior formalization). The Rado/ development follows their Perron treatment (Definition 2, Proposition 3, Remark 4, Theorem 6, Theorem 7) with formalization-motivated deviations recorded in Rado/PLAN.md: explicit two-disk configuration with log-barriers instead of general Dirichlet boundary regularity, and an étale space of exact harmonic-conjugate germs instead of the universal cover. - title: "Teichmüller theory and applications to geometry, topology, and dynamics, Vol. 1, §1.2-1.3" authors: ["John Hamal Hubbard"] id: "Matrix Editions (2006) — the eval problem's cited source; freely available Chapter 1 excerpt consulted" type: "book" license: "" author_contacted: "n/a" prior_work: "" - title: "Lectures on Riemann Surfaces, §22-23 (via Armin Rainer's lecture notes)" authors: ["Otto Forster", "Armin Rainer"] id: "Springer GTM 81; Rainer's Vienna notes — source for the Poincaré-Volterra lemma (23.2) and Dirichlet problem (22.3)" type: "book / lecture notes" license: "" author_contacted: "n/a" prior_work: "" - title: "Formalizing Pick's Theorem, efficiently" authors: ["Michael Eisermann", "Roland Zumkeller", "et al."] id: "arXiv:2603.23095 (2026)" type: "paper / prior Lean formalization (partial)" license: "" author_contacted: "no" prior_work: > Clean-room with respect to proofs. Their development proves the algebraic count identity but leaves the geometric half (a winding/Umlaufsatz argument) unproved (sorry). The count side here (latWeight / latWeightSum in Weight.lean) follows their discrete-angle-weight device (dang / Welp); the per-edge identity is proved independently (a column decomposition rather than their four-box partition + reflection involution) — see the Weight.lean header. - title: "The Jordan curve theorem via the Brouwer fixed point theorem" authors: ["Ryuji Maehara"] id: "Amer. Math. Monthly 91 (1984), 641-643; doi:10.2307/2323369" type: "paper" license: "" author_contacted: "n/a" prior_work: "" - title: "Polygons Have Ears" authors: ["Gary H. Meisters"] id: "Amer. Math. Monthly 82(6) (1975), 648-651; doi:10.2307/2319703" type: "paper (the two-ears theorem behind the ear-clipping reduction)" license: "" author_contacted: "n/a" prior_work: "" - title: "A formal proof of Pick's theorem" authors: ["John Harrison"] id: "Math. Struct. Comput. Sci. (2011)" type: "prior formalization (HOL Light)" license: "" author_contacted: "n/a" prior_work: "consulted as prior art only; no code ported" - title: "Formalizing Pick's Theorem in Isabelle/HOL" authors: ["Sage Binder", "Katherine Kosaian"] id: "CICM 2024; arXiv:2405.01793; AFP entry Picks_Theorem" type: "prior formalization (Isabelle/HOL)" license: "" author_contacted: "n/a" prior_work: "consulted as prior art only; no code ported" status: scope: > COMPLETE. Pick's theorem (Freek's Formalizing 100 Theorems #92) for simple lattice polygons with area as genuine Lebesgue measure (area = I + B/2 − 1), the polygonal Jordan curve theorem (winding ∈ {0,1}, complement has at most two components), the full continuous Jordan curve theorem (a continuous injection S¹ → ℝ² has a complement with exactly two connected components), the 2-D Brouwer fixed point theorem, and Radó's theorem (every connected Hausdorff Riemann surface is second countable) — all missing from Mathlib. All three lean-eval problems (pick, jordan_curve, rado_riemannSurface) are proved in their exact harness statements against the harness's pinned toolchain (Lean v4.32.2, Mathlib 905b9581); the rado_riemannSurface submission passed the lean-eval comparator (2026-07-10). sorry_count: 0 # scope: the submitted results and the JordanPick/ + Rado/ # libraries they are built from. The in-progress # Uniformization/ development is NOT covered -- see # in_progress below. sorry_in_definitions: 0 axioms: # scope as for sorry_count: the axiom surface of every # declaration in JordanPick/ and Rado/, hence of all # submitted results. Uniformization/ is not covered. - "propext" - "Classical.choice" - "Quot.sound" in_progress: # not submitted; recorded so the counts above are not # mistaken for a repo-wide claim - directory: "Uniformization/" goal: "lean-eval `uniformization` (Hubbard Thm 1.1.2)" sorry_count: 2 sorries: - declaration: "LeanEval.Geometry.isFreeGroup_fundamentalGroup" file: "Uniformization/Main.lean" missing_input: > pi_1 of an open surface is free (Ahlfors-Sario 1960 sec. 44A), reached by Rado triangulability of open surfaces plus Whitehead's spine. Neither is in Mathlib at the pin. Everything downstream of it is proved sorry-free in Uniformization/Pi1Free.lean, so LeanEval.Geometry.uniformization is proved modulo this one input. - declaration: "Uniformization.exists_end_collapse" file: "Uniformization/Surface/Fill/Collapse.lean" missing_input: > A TubeData: two-sided tubular neighbourhood of the cutting ray. The chain TubeData -> RayCollar -> exists_end_collapse is complete and sorry-free. notes: > Because of these, LeanEval.Geometry.uniformization_key and LeanEval.Geometry.uniformization depend on sorryAx via exists_end_collapse; they are NOT axiom-clean, unlike the submitted results above. main_results: - declaration: "LeanEval.Geometry.PicksTheorem.pick" file: "JordanPick/PicksTheorem/EvalBridgeMain.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "submission/pick/config.json" literature_dependencies: [] - declaration: "JordanCurve.jordan_curve" file: "JordanPick/JordanCurve.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "submission/jordan_curve/config.json" literature_dependencies: [] - declaration: "Pick.pick" file: "JordanPick/PicksTheorem/Pick.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "" literature_dependencies: [] - declaration: "Pick.LatticePolygon.compl_boundary_atMost_two" file: "JordanPick/PicksTheorem/Pick.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "" literature_dependencies: [] - declaration: "JordanCurve.Brouwer.brouwerFPT" file: "JordanPick/JordanCurve/Brouwer.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "" literature_dependencies: [] - declaration: "rado_riemannSurface" file: "Rado/Main.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "submission/rado_riemannSurface/config.json" literature_dependencies: - "arXiv:2008.12189 (Anghel–Stan): Perron treatment" - "Forster GTM 81 §22-23 / Rainer notes: Poincaré–Volterra (23.2), Dirichlet problem (22.3)" - "Hubbard, Teichmüller theory Vol. 1 §1.3: the eval problem's cited source" automation: methods: - method: "autonomous" # agentic formalization: high-level human prompts; Claude Code drives end-to-end models: ["claude-fable-5", "claude-opus-4-8"] framework: "Claude Code" tool_setup: > Claude Code with background sub-agent orchestration; soundness gate: every claimed close is independently kernel-verified via `#print axioms` (sorryAx must be absent) before being trusted; each commit is `lake build`-green. Heartbeat/performance passes are profiler-driven (`#count_heartbeats` with Elab.async off, `set_option diagnostics true`). cost: wall_time: "assembled repo history 2026-06-26 to 2026-07-02 (development predates the assembled history)" spend_usd: "subscription-based usage, $100/month subscription" hardware: "single 4-core / ~8 GB laptop; API-only model access" prompting_notes: > Steered with terse high-level directives; discipline encoded in project memory: connect already-proven pieces bottom-up, verify every agent commit by kernel axiom checks, flag (don't fake) false-as-stated statements. spend_usd: "subscription-based usage" notes: > ~33.5k lines of Lean code across 38 files (JordanPick: Pick + Jordan/Brouwer; Rado: Radó's theorem), sorry-free, zero custom axioms, zero compiler warnings, and no maxHeartbeats overrides (every proof fits the default 200k budget). The Rado development is warned-free with `autoImplicit false` throughout and #lint clean. fidelity: divergences: > Area in Pick's theorem is the genuine Lebesgue measure of the winding interior — NOT shoelace-as-definition; the shoelace identity is proved (Green: area = ∫∫ winding = shoelace). The spine is the winding number as a per-edge signed ray-crossing sum (pure integer arithmetic — no transcendental angles, no general topology); the polygonal JCT follows a crossing-alternation route; the area identity reduces to triangles by ear-clipping induction (Meisters two-ears via a deepest-contained-vertex diagonal split). The continuous JCT is a separate development (independent of the polygonal one): Maehara's Brouwer-based proof, with Brouwer built from the ground up (covering-space path lifting for the circle, no-retraction, ray-retraction on the disk, nearest-point projection for convex compacts). The lean-eval bridge matches the harness statements verbatim (Mathlib Polygon, topological interior, no orientation hypothesis). Radó's theorem follows Anghel–Stan's Perron treatment with two formalization-motivated deviations (recorded in Rado/PLAN.md, route "A′"): an explicit two-disk configuration with log-barriers (unit disks at ±4 inside chart ball B(0,8), witnesses at ±4 + 2^(1/4)) in place of general Dirichlet boundary regularity, and an étale space of exact harmonic-conjugate germs (Re F = u exactly; sheets differ by imaginary constants) in place of the universal cover, with descent via Poincaré–Volterra. The harness statement is proved verbatim (connected Hausdorff ChartedSpace ℂ with IsManifold ⟹ SecondCountableTopology, pure Mathlib). review: status: "self-assessed" reviewers: [] notes: > Verification is by Lean's kernel: `#print axioms` on every main result (all report [propext, Classical.choice, Quot.sound], no sorryAx), the full `lake build` (green, zero warnings), and the repo-wide zero-sorry sweep. The rado_riemannSurface submission additionally passed the lean-eval comparator (2026-07-10), which independently re-checks the axiom surface against the permitted set. No external peer review yet; expert review is welcome (Junyan Xu has expressed interest in upstreaming the Radó pieces — Poincaré–Volterra, the Dirichlet disk solution, and Perron — to Mathlib). alignment: namespace: "Pick (Pick's theorem + polygonal JCT), JordanCurve (continuous JCT + Brouwer), LeanEval.Geometry.PicksTheorem (eval bridge), Rado (Radó's theorem), root rado_riemannSurface (eval statement)" statements: - source: "lean-eval pick — https://lean-lang.org/eval/problems/pick/" lean: "LeanEval.Geometry.PicksTheorem.pick" module: "JordanPick/PicksTheorem/EvalBridgeMain.lean" status: "proved" note: "exact harness statement (Mathlib Polygon, topological interior, no orientation hypothesis), bridged to Pick.pick" - source: "lean-eval jordan_curve — https://lean-lang.org/eval/problems/jordan_curve/" lean: "JordanCurve.jordan_curve" module: "JordanPick/JordanCurve.lean" status: "proved" note: "exact harness statement: Nat.card (ConnectedComponents (range r)ᶜ) = 2 for a continuous injection r : sphere 0 1 → ℝ²" - source: "Freek Wiedijk, Formalizing 100 Theorems #92 (Pick's theorem)" lean: "Pick.pick" module: "JordanPick/PicksTheorem/Pick.lean" status: "proved" note: "area = I + B/2 − 1 with area the Lebesgue measure of the winding interior" - source: "Polygonal Jordan curve theorem" lean: "Pick.LatticePolygon.compl_boundary_atMost_two" module: "JordanPick/PicksTheorem/Pick.lean" status: "proved" note: "complement of a simple polygon's boundary has at most two components; winding locally constant ∈ {0,1}" - source: "Brouwer fixed point theorem (2-D, convex compact)" lean: "JordanCurve.Brouwer.brouwerFPT" module: "JordanPick/JordanCurve/Brouwer.lean" status: "proved" note: "self-contained against Mathlib: covering-space path lifting → no-retraction → disk → convex compact" - source: "lean-eval rado_riemannSurface — https://lean-lang.org/eval/problems/rado_riemannSurface/" lean: "rado_riemannSurface" module: "Rado/Main.lean" status: "proved" note: "exact harness statement: a connected T2 ChartedSpace ℂ that IsManifold (𝓘(ℂ,ℂ), 1) has SecondCountableTopology; comparator-passed 2026-07-10, bridged to Rado.secondCountableTopology_of_riemannSurface" - source: "Radó's theorem (Riemann surfaces are second countable)" lean: "Rado.secondCountableTopology_of_riemannSurface" module: "Rado/Surface/Assembly.lean" status: "proved" note: "Perron on a two-disk configuration → étale space of exact harmonic-conjugate germs → Poincaré–Volterra → descent (route A′, Rado/PLAN.md)" acknowledgements: > Built on Mathlib (Lean 4, pin 905b9581). The count-side discrete-angle-weight device follows Eisermann & Zumkeller (arXiv:2603.23095); the Radó development follows the Perron treatment of Anghel & Stan (arXiv:2008.12189) with the Poincaré–Volterra lemma and Dirichlet problem from Forster (GTM 81 §22-23, via Rainer's notes) and Hubbard's Teichmüller theory §1.3 as the cited source; everything else is clean-room, with prior formalizations (Harrison HOL Light 2011, Binder-Kosaian Isabelle/HOL 2024) credited as prior art. Eval problem statements by the Lean FRO (leanprover/lean-eval); the rado_riemannSurface problem was submitted by Junyan Xu.