Li Proof Library

Proof library

Dedicated home for Li's proof corpus — separate from benchmark wall-clock ratios. Compare scientific catalog opinion (TOML / proof-db) vs Lean scan, then vote what you believe.

Catalog — proof_status in lic/docs/verification/proof-database/
Lean — static scan of theorem bodies in lic semantics
Red row — catalog and Lean disagree

Compiler gaps: provability-gaps.md

G-* compiler gaps

G-ann: MissingG-async: PartialG-authz: MissingG-bnd: PartialG-dec: PartialG-def: Partial+G-gpu: MissingG-hw: AxiomaticG-lean: PartialG-math: PartialG-math-syn: PartialG-meta: MissingG-narrow: PartialG-net: Partial

Scientific opinion = catalog / TOML proof_status (what we claim in the proof database). Lean opinion = static scan of theorem bodies in lic semantics (sorry → open, axiom → axiomatic).

Generated 2026-05-29T19:03Z · lic 3e21dd9a · 36 entries · 6 divergent

Votes persist in this browser only until a shared tally backend ships.

Catalog

axiomatic 10
open 9
proved 16
discrepancy 1

Lean scan

axiomatic 15
unknown 6
proved 11
placeholder 4

SearchFieldDivergent only36 / 36 shown

ID	Statement	Catalog	Lean	Gap	Your vote
A-trusted-getelem trust · axiom source	typing_getElem trusted.	axiomatic	axiomatic	G-trust	Discuss on GitHub
G-lean-autovc-strict compiler · lemma source	No open Prop without _proved. li-tests/contracts_verify/discharge_trivial.li	open	unknown	G-lean	Discuss on GitHub
M-AX-ORDER-ANTISYM math · axiom source	Order: antisymmetry on Nat (≤). proof-db/math/axioms/peano_order.li	axiomatic	axiomatic	G-math axiom_layer	Discuss on GitHub
M-AX-ORDER-TRICHOTOMY math · axiom source	Order: trichotomy on Nat (<, =, >). proof-db/math/axioms/peano_order.li	axiomatic	axiomatic	G-math axiom_layer	Discuss on GitHub
M-AX-PEANO-IND math · axiom source	Peano: induction schema on Nat. proof-db/math/axioms/peano_order.li	axiomatic	axiomatic	G-math axiom_layer	Discuss on GitHub
M-AX-PEANO-SUCC-INJ math · axiom source	Peano: successor is injective on Nat. proof-db/math/axioms/peano_order.li	axiomatic	axiomatic	G-math axiom_layer	Discuss on GitHub
M-AX-PEANO-ZERO-NOT-SUCC math · axiom source	Peano: zero is not a successor. proof-db/math/axioms/peano_order.li	axiomatic	axiomatic	G-math axiom_layer	Discuss on GitHub
M-AX-REAL-ADD-ASSOC math · axiom source	ℝ field: addition associative. proof-db/math/axioms/reals_field.li	axiomatic	axiomatic	G-math axiom_layer	Discuss on GitHub
M-AX-REAL-ADD-COMM math · axiom source	ℝ field: addition commutative. proof-db/math/axioms/reals_field.li	axiomatic	axiomatic	G-math axiom_layer	Discuss on GitHub
M-AX-REAL-MUL-DIST math · axiom source	ℝ field: multiplication distributes over addition. proof-db/math/axioms/reals_field.li	axiomatic	axiomatic	G-math axiom_layer	Discuss on GitHub
M-AX-REAL-MUL-ONE math · axiom source	ℝ field: multiplicative identity 1. proof-db/math/axioms/reals_field.li	axiomatic	axiomatic	G-math axiom_layer	Discuss on GitHub
M-LM-ADD-ASSOC math · lemma source	Real addition associative (discharged from M-AX-REAL-ADD-ASSOC). proof-db/math/axioms/reals_field.li	proved	proved	G-math proof_gap	Discuss on GitHub
M-LM-ADD-COMM math · lemma source	Real addition commutative (discharged from M-AX-REAL-ADD-COMM). proof-db/math/axioms/reals_field.li	proved	proved	G-math proof_gap	Discuss on GitHub
M-LM-FLOAT-ADD-COMM math · lemma source	Float add_commutative specimen vs ℝ axiom (catalog discrepancy). Specimen ensures float add comm; triage under backlog P-float — not a compiler wrongness verdict. proof-db/math/lemmas/add_commutative.li	discrepancy	axiomatic≠	G-math numerics_gap	Discuss on GitHub
M-LM-MUL-ONE math · lemma source	Real multiply-by-one (discharged from M-AX-REAL-MUL-ONE). proof-db/math/axioms/reals_field.li	proved	proved	G-math proof_gap	Discuss on GitHub
M-LM-NAT-ADD-COMM math · lemma source	Nat: addition commutative (Peano + order layer). proof-db/math/axioms/peano_order.li	proved	proved	G-math proof_gap	Discuss on GitHub
M-LM-NAT-ADD-ZERO math · lemma source	Nat: n + 0 = n (Peano layer target). proof-db/math/axioms/peano_order.li	proved	proved	G-math proof_gap	Discuss on GitHub
P-AX-CONS-001 physics · axiom source	Energy drift within a bounded window over one MD step (tier-0 smoke + tier-2 MD). proof-db/physics/axioms/conservation.li	open	axiomatic≠	G-physics modeling_gap	Discuss on GitHub
P-AX-CONS-002 physics · axiom source	Linear/angular momentum invariants for N-body integration (tier-0 + tier-2). proof-db/physics/axioms/conservation.li	open	axiomatic≠	G-physics modeling_gap	Discuss on GitHub
P-AX-DIM-001 physics · axiom source	Dimensional homogeneity: only dimensionally consistent combinations are well-formed.	open	placeholder	G-physics proof_gap	Discuss on GitHub
P-AX-DIM-002 physics · axiom source	SI coherence: base quantities map to a consistent unit system (placeholder).	open	placeholder	G-physics proof_gap	Discuss on GitHub
P-AX-MECH-001 physics · axiom source	Newton I (inertia): isolated body with zero net force has constant velocity. proof-db/physics/axioms/newton_laws.li	open	axiomatic≠	G-physics modeling_gap	Discuss on GitHub
P-AX-MECH-002 physics · axiom source	Newton II: net force equals mass times acceleration (scalar stub). proof-db/physics/axioms/newton_laws.li	open	placeholder	G-physics proof_gap	Discuss on GitHub
P-AX-MECH-003 physics · axiom source	Newton III (action–reaction): interaction forces on a pair sum to zero. proof-db/physics/axioms/newton_laws.li	open	axiomatic≠	G-physics modeling_gap	Discuss on GitHub
P-LM-CONS-001 physics · lemma source	Closed-system energy and momentum invariants compose from MECH + CONS axioms (integrator window). proof-db/physics/lemmas/energy_drift_bound.li	open	unknown	G-physics modeling_gap	Discuss on GitHub
P-LM-ENERGY-001 physics · lemma source	Kinetic energy T = ½ m v² consistent with scalar speed squared.	proved	proved	G-physics none	Discuss on GitHub
P-LM-MOM-001 physics · lemma source	Linear momentum p = m v for point mass.	proved	placeholder≠	G-physics none	Discuss on GitHub
P-discharge-trivial compiler · lemma source	Trivial discharge. li-tests/contracts_verify/discharge_trivial.li	proved	unknown	G-lean	Discuss on GitHub
P-float-sqrt-open-bound math · lemma source	sqrt_open_bound. li-tests/contracts_verify/sqrt_open_bound.li	proved	unknown	G-math	Discuss on GitHub
P-linalg-dot4-int-closed linalg · lemma source	Fixed 4-term int dot closed witness. li-tests/contracts_verify/linalg_dot4_int_closed.li	proved	unknown	G-math	Discuss on GitHub
P-linalg-dot4-int-loop-open linalg · lemma source	Loop dot4 int closed. li-tests/contracts_verify/linalg_dot4_int_loop_open.li	proved	unknown	G-math	Discuss on GitHub
std_add_comm stdlib · lemma source	∀ a b ∈ ℤ, a + b = b + a	proved	proved	—	Discuss on GitHub
std_dot4_bilinear_right stdlib · lemma source	⟨a,b+c⟩ = ⟨a,b⟩+⟨a,c⟩	proved	proved	—	Discuss on GitHub
std_dot4_comm stdlib · lemma source	⟨a,b⟩ = ⟨b,a⟩	proved	proved	—	Discuss on GitHub
std_mul_assoc stdlib · lemma source	∀ a b c ∈ ℤ, (a·b)·c = a·(b·c)	proved	proved	—	Discuss on GitHub
std_triangle_ineq_scalar stdlib · lemma source	∀ a b, \|a+b\| ≤ \|a\|+\|b\|	proved	proved	G-hw	Discuss on GitHub