A formal verification of Linear PCP SNARKs.

Riemann Hypothesis in Lean

Lean4 kernel for synthetic formalization and discovery of statistical learning theory. First and complete formalization of the 5 way fundamental theorem. Typed premise + human-guided, AI-driven proof search across PAC, online, and Gold paradigms. The infrastructure forced by the types produced original mathematics.

📏 A dependently-typed language on Lean 4 for formalizing physics. Dimensions, uncertainty & theory conflicts are first-class types. 25 domains, 267 theorems, 0 sorry. Theories can conflict, approximate or extend each other — because physics isn't one consistent system. Compilation = proof.

A Lean 4 library for formal linguistics.

A formalization of graded rings in Lean, corresponding to a CICM 2022 submission

University Master Thesis

A formalization of chip-firing games and the Riemann-Roch theorem for graphs using the Lean 4 theorem prover.

Lean 4 Theoretical Computer Science Library

Lean 4 + Mathlib formalization: (u,v)-flower graph construction, hub distance = u^g, and log-ratio convergence to log(u+v)/log(u)

Lean 4 + Mathlib formalization of delay embedding theory for dynamical systems

Machine-verified proof (0 sorries, 2 axioms) that P ≠ NP via exponential circuit lower bounds for Hamiltonian Cycle. Lean 4 formalization with Mathlib. Proves SIZE(HAM_n) ≥ 2^{Ω(n)} using frontier analysis, switch blocks, cross-pattern mixing, recursive funnel magnification, continuation packets, rooted descent, and signature rigidity.

The Beal Symmetry Collision: A Machine-Certified Solution via p-adic Valuations

Machine-checked Lean 4 proofs for "Language Model Hallucinations: An Impossibility Theorem and Its Architectural Consequences." Covers Theorem 1 (impossibility of guaranteed consistency), certification-depth lower bounds, mitigation boundaries for CoT / grammar / rerank, and intrinsic/extrinsic DCF taxonomy.

Deterministic, auditable Lean 4 + mathlib reasoning instrument (not an oracle): contracts, assumption surfacing, reduction scaffolds, dashboard + PDF reports.

Lean 4 + Mathlib formalization of the Creative Determinant framework — 15 theorems proved with zero sorry, CI-enforced via lake build --wfail

Machine-checked Lean 4 proofs for "Path-Game GAF Pilot v0.1: Cross-Provider Program Handoff v1.7" — hamiltonian-path as abstract ConstraintSystem instance (inheriting Sudoku-Microscope theorems) and Layer 2 silent-commit signature formalization with provider-agnostic well-definedness.

Formal Proof of the Non-Existence of Perfect Cuboids via Mordell-Weil Rank Exhaustion and Minimal Polynomial Irreducibility of the Perfect Cuboid Surface.

Machine-checked Lean 4 proofs for "From Recursive Scaffolding to Admissibility-First Construction: Mechanism, Stability, and Failure-Mode Decomposition on OOLONG-Pairs" — filter recall preservation, oracle construction sufficiency, endpoint-factorization insufficiency, and pair-precision amplification under independence.

Machine-checked Lean 4 proofs for "Sudoku as a Microscope for Non-Extendable Commitment: Empirical Validation of Global Admissibility Filtering" — local-global separation, catastrophic commitment foreclosure, forced-gate safety, and bucket sufficiency in abstract constraint systems.