Kleis
Universal Verification Platform for Mathematics, Business Rules, and Beyond
🔬 Type System
Hindley-Milner type inference with complete algebraic foundations
🎯 Verification
Z3 theorem prover integration for axiom verification
🌐 Universal
Mathematics, business rules, network protocols, and more
📝 Self-Hosting Architecture
Bootstrap in Rust, extensible in Kleis
📄 Research
Machine-verified papers produced entirely in Kleis — axioms, proofs, numerics, and typesetting from a single reproducible source.
Identifies the completed zeta function ξ(s) with the characteristic polynomial of an antisymmetric matrix. Six theorems, machine-checked in Lean 4, verified by Z3. 11 pages. View source (.kleis)
Reframes the spectral comb as a state-space realization of 1/ζ(s). Antisymmetry forces Re = 1/2 by a one-line identity; convergence covered by Connes' theorem and six published spectral approximation results. 18 references, 13 executable tests. View source (.kleis)
Derives flat rotation curves and the Tully-Fisher relation (M ∝ v⁴) without dark matter. 14 axioms, 4 theorems, all verified by Z3. View source (.kleis)