"Type Theory and Formal Proof: An Introduction" book formalization in Lean
-
Updated
Aug 26, 2025 - Lean
#
formal-proof
Here are 23 public repositories matching this topic...
Sort: Most stars
Sort options
Vyukov MPSC queue in C++20 with a six-claim formal memory-model proof, push_batch API (Claim 6), 53M msg/sec at 4 producers, 18 TSan litmus tests, and a software tick-to-trade benchmark.
-
Updated
Sep 7, 2026 - C++
Lean formalization of MEV properties.
smart-contracts formalization amm mev lean4 automated-market-maker formal-proof maximal-extractable-value
-
Updated
Dec 24, 2025 - Lean
A complete Lean 4 formalization of the nonsingularity of Colombo's 1928 difference-power determinant.
-
Updated
Aug 28, 2026 - Lean
A formal proof, in LaTeX, that 3-Partition is NP-complete in the strong sense, following the Garey and Johnson reduction chain. MAC coursework, UGR.
-
Updated
Aug 17, 2026 - TeX
Formal Proof of the Non-Existence of Perfect Cuboids via Mordell-Weil Rank Exhaustion and Minimal Polynomial Irreducibility of the Perfect Cuboid Surface.
lift singularity computational-mathematics modular-arithmetic algebraic-geometry number-theory interactive-theorem-proving hyperelliptic-curves mathlib lean4 diophantine-equations euler-bricks lll-algorithm formal-proof perfect-cuboid tate-shafarevich mordell-weil-theorem jacobian-analysis faltings-theorem irreducibility
-
Updated
Jul 18, 2026 - Lean
Formal Verification of the 7-Color Chromatic Number of the Plane via Toroidal Projection and the Irrationality of 2π.
graph-theory formal-verification interactive-theorem-proving irrationality mathlib zulip-bot chromatic-number de-bruijn lean4 2pi formal-proof k-colorability toroidal-topology hadwiger-nelson-problem moser-spindle unit-distance-graph pigeonhole-principle proof-by-exclusion
-
Updated
Jul 20, 2026 - Lean
First Lean formalization of 200 measured Hodge (2,2)-class obstructions on CM abelian varieties. Clay Wall 3. Applied science: numerical ranks > bounds for g=3,4,5. 0 axiom. 0 sorry.
lean lean4 formal-proof hodge-conjecture abelian-varieties clay-millennium applied-algebraic-geometry cm-abelian-varieties
-
Updated
Aug 24, 2026 - Lean
Route C of 4 — Act III Growth. RH via contradiction: |ζ|≤C(log t)2 false via Littlewood 1924 Ω exp(c√(log t/log log t)). Zero repulsion c1=0.209>0.2 β>0.9 closed at p5 → S4={2,3,19,191} C=11.422>2√13 → GRH → H4 12/11 → RH. Lean 4.12 0 sorry. Opera Numerorum with A, B, D 35 brothers desert.
riemann-zeta number-theory mathlib grh riemann-hypothesis analytic-number-theory littlewood lean4 riemann-zeta-function formal-proof riemann-hypothesis-lean4-mathematics riemann-zeta-constant bost-connes x0-143 riemann-zeta- kronecker-theorem omega-result zero-repulsion
-
Updated
Aug 24, 2026 - Lean
Route B of 4 — Act II Descent. RH via spectral gap X0(143) λ1≥975/4096 Kim-Sarnak → Selberg = Bost-Connes C(S4)=11.422>2√13 → GRH → H4 12/11 → RH. 35pp BC6 20450 bytes 0 sorry. Opera Numerorum with A ω2=48/13>0, C Littlewood Ω, D 35 brothers jitter ||p·α0||<1/p → R=1/2. doi:10.5281/zenodo.21303976
-
Updated
Aug 24, 2026 - Lean
ia Collapse Theory and AK High-Dimensional Projection This repository presents Version 2.0 of a formal, categorical, and type-theoretic resolution of the Hodge Conjecture, formulated through Collapse Theory and the AK High-Dimensional Projection Structural Framework (AK-HDPST).
category-theory algebraic-geometry persistent-homology formal-proof hodge-conjecture collapse-theory ak-theory high-dimensional-projection ext-class
-
Updated
Jul 15, 2025 - TeX
Route A of 4 — Act I Positivity. RH via Arakelov on X0(143) g=13 ω2=48/13>0 Abbes-Ullmo 1996 → S4={2,3,19,191} C=11.422>2√13 → GRH M9 → H4 12/11 → RH. Lean 4.12 0 sorry riemannZeta. Opera Numerorum with B λ1≥975/4096, C exp(c√log/loglog), D jitter ||p·α0||<1/p → R=1/2. doi:10.5281/zenodo.21303944
-
Updated
Aug 24, 2026 - Lean
Kernel-checked Lean 4 proof that no infinite simple paramedial quasigroups exist (Loops '03 open problem).
theorem-proving abstract-algebra mathlib quasigroup universal-algebra nonassociative-algebra lean4 formal-proof open-problem loop-theory paramedial
-
Updated
Jul 23, 2026 - Lean
A formal constructive proof of the Goldbach Conjecture using A-type primes. The theory guarantees every even number ≥4 can be expressed as a sum of two primes, offering a reproducible and extendable number-theoretical foundation. A型素数を用いた構成的手法により、すべての偶数(4以上)が2つの素数の和で表現可能であることを証明。再現性と拡張性を兼ね備えた数論的基盤を提供します。
reproducible-research prime-numbers number-theory goldbach-conjecture constructive-mathematics formal-proof
-
Updated
Jun 23, 2025
Esolang de reescritura de cadenas cuyo alfabeto son repeticiones del token 'ja'. Turing completo, con prueba ejecutable.
-
Updated
Sep 4, 2026 - Python
Lean 4 unconditional proof: riemann_hypothesis_unconditional (B158). 0 sorry, 0 axiom beyond classical trio. 18 minimum sub-atoms proved. Opera Numerorum -- David Fox. DOI: 10.5281/zenodo.20981649
-
Updated
Aug 29, 2026 - Lean
This repository presents a constructive solution to the Yang–Mills existence and mass gap problem, a Clay Millennium Prize topic. The framework confirms the existence of a positive mass gap through verifiable quantum field logic. 本リポジトリでは、クレイ懸賞問題のひとつであるヤン–ミルズ存在と質量ギャップ問題に対し、構成的に正の質量ギャップの存在を示す理論を収録しています。量子場理論に基づき、検証可能な構成を整備しています。
quantum-field-theory mathematical-physics millennium-problems constructive-mathematics yang-mills-theory formal-proof mass-gap
-
Updated
Jun 23, 2025
Proof of Constitutional Enclosure Theorem: silent AI decisions are type errors
-
Updated
Aug 27, 2026 - TeX
Standalone Lake projects for Mathlib-adjacent experiments (Euler's polyhedron formula via convex polyhedra and combinatorial maps)
-
Updated
Sep 1, 2026 - Lean
本项目用 Lean4 形式化验证一个红蓝选择问题中的理由结构。项目关注的不是玩家实际会如何选择,而是: 在给定价值准则、背景条件和理由生成规则下,某个策略是否能够成为某个玩家的最终合理策略。
-
Updated
May 4, 2026 - TeX
Add this topic to your repo
To associate your repository with the formal-proof topic, visit your repo's landing page and select "manage topics."