An SMT solver in Rust that proves its answers: QF_UF, QF_LRA, QF_LIA, QF_NRA, QF_BV, with LRAT and Alethe proofs.
-
Updated
Oct 9, 2026 - Rust
An SMT solver in Rust that proves its answers: QF_UF, QF_LRA, QF_LIA, QF_NRA, QF_BV, with LRAT and Alethe proofs.
A machine-checked ledger of covering-code upper bounds K_q(n,R), with formally certified exact entries in Lean 4.
Research preview: Axis-Servant bound, LRAT-refuted 6x4 support formula, and 6x3 frontier lemma
CC0 candidate proofs for z(20)=6 and VR2(K4)=20, with replayable certificates and AI-readable indexes
SAT + verified LRAT certificate for a covering-system lower bound (Erdős #273), plus a segmented sieve extending verified ranges for #385 and #647 to 1.0011e12
To associate your repository with the lrat topic, visit your repo's landing page and select "manage topics."