Latest run: 2026-04-27T18:34:38Z
Summary: 35/35 passing, 0 regressed, 0 failing, 0 in-progress, 0 stub, 0 not-started, 0 prover-missing.
| ID | Theorem | Prover | Status | Semantic | Elapsed (ms) |
|---|---|---|---|---|---|
M1 |
Infinitude of primes (Euclid) |
idris2 |
passing |
verified |
8482 |
M2 |
Lagrange’s theorem (group order divides) |
rocq |
passing |
verified |
6143 |
M3 |
Intermediate value theorem (continuous real-valued) |
rocq |
passing |
verified |
2148 |
M4 |
Compactness of [0,1] (Heine-Borel for closed unit interval) |
rocq |
passing |
verified |
2877 |
M5 |
Yoneda lemma (locally small categories) |
agda |
passing |
verified |
1190 |
S1 |
Conservation of energy from time-translation invariance (Noether classical case) |
rocq |
passing |
verified |
385 |
S2 |
Gauss’s law (Maxwell, differential form, vacuum) |
rocq |
passing |
verified |
414 |
S3 |
H-theorem re-scope: binary-distribution entropy proxy p*(1-p) is maximised at uniform p = 1/2 (value 1/4) |
rocq |
passing |
verified |
1637 |
S4 |
Heisenberg uncertainty re-scope: discrete Cauchy-Schwarz on R^2 (finite-dimensional kernel of the operator-algebra derivation) |
rocq |
passing |
verified |
1286 |
S5 |
Shannon source-coding (rate >= entropy is necessary) |
rocq |
passing |
verified |
1272 |
E1 |
Lyapunov stability of n-dim LTI system: V_of P (traj_infty A x0 t) ⇐ V_of P x0 for the explicit trajectory x(t) = exp(tA) x0, under positive_definite P and negative_definite (Aᵀ P + P A) |
rocq |
passing |
verified |
3863 |
E2 |
Equivalence of two adder designs (ripple-carry vs carry-lookahead, single bit-width) |
idris2 |
passing |
verified |
3465 |
E3 |
Bound on cantilever beam deflection (Euler-Bernoulli, single point load) |
rocq |
passing |
verified |
180 |
E4 |
Correctness of merge sort (output is sorted permutation of input) |
idris2 |
passing |
verified |
3528 |
E5 |
Needham-Schroeder fix re-scope: challenge-response key-binding under injective MAC (core cryptographic fact Lowe’s fix relies on) |
rocq |
passing |
verified |
170 |
M6 |
Deduction theorem / modus ponens closure (propositional logic) |
rocq |
passing |
verified |
172 |
S6 |
Law of mass action: equilibrium condition for an elementary reaction |
rocq |
passing |
verified |
230 |
E6 |
CSTR steady-state mass balance closure (chemical engineering) |
rocq |
passing |
verified |
253 |
M7 |
Linearity of expectation (finite discrete random variables) |
rocq |
passing |
verified |
212 |
M8 |
Rank-nullity theorem for finite-dimensional linear maps |
rocq |
passing |
verified |
698 |
M9 |
Unique factorization in a UFD (integers as base case) |
rocq |
passing |
verified |
425 |
M10 |
Connected sum of knots forms a commutative monoid with unknot as identity |
rocq |
passing |
verified |
187 |
M11 |
Pigeonhole principle (finite case, arbitrary surjection) |
rocq |
passing |
verified |
691 |
E7 |
Carnot efficiency upper bound for a heat engine between two reservoirs |
rocq |
passing |
verified |
145 |
S7 |
Lorentz-boost composition / relativistic velocity addition (special relativity) |
rocq |
passing |
verified |
179 |
E8 |
Nyquist-Shannon sampling theorem: 2W sufficient rate for bandlimited reconstruction |
rocq |
passing |
verified |
171 |
M12 |
Dominated convergence theorem (Lebesgue integration) |
rocq |
passing |
verified |
205 |
S8 |
Hardy-Weinberg equilibrium stability under random mating (population genetics) |
rocq |
passing |
verified |
171 |
E9 |
Newton’s method local quadratic convergence (numerical analysis) |
rocq |
passing |
verified |
194 |
M13 |
Hahn-Banach extension theorem (functional analysis) |
rocq |
passing |
verified |
209 |
M14 |
Max-flow / min-cut duality (graph theory) |
rocq |
passing |
verified |
174 |
S9 |
Chandrasekhar mass upper bound for white-dwarf stars (astrophysics) |
rocq |
passing |
verified |
171 |
S10 |
R_0 threshold for endemic-equilibrium existence (compartmental epidemiology) |
rocq |
passing |
verified |
172 |
E10 |
Weibull / bathtub-curve failure-rate bound (reliability engineering) |
rocq |
passing |
verified |
144 |
E11 |
Kirchhoff voltage + current laws for lumped-element circuits |
rocq |
passing |
verified |
165 |