Formal Verification Certificate
All theorems formally verified in Lean 4 with zero sorry gaps.
Semi-Algebraic Lean • Lean 4 + Mathlib • Apoth3osis Labs
The Central Question
Can a machine decide whether a system of polynomial inequalities has a real solution? Yes — Tarski proved in 1951 that the first-order theory of the reals is decidable. This project formalizes the decision procedure in Lean 4: given a quantifier-free system of polynomial constraints over ℜ, it either finds a satisfying point or produces a Positivstellensatz refutation proving no solution exists. The machinery — cylindrical algebraic decomposition, Sturm chains, sign determination — is all machine-checked.
Key Verified Results
tarski_decidableFirst-order theory of reals is decidable
Decidability.lean
cad_correctCAD decomposes ℝⁿ into sign-invariant cells
CAD.lean
sat_certificate_soundSAT witness satisfies all constraints
Certificate.lean
unsat_certificate_soundPositivstellensatz refutation proves infeasibility
Certificate.lean
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.
Contribution Certificates
Immutable contribution records per MENTAT-CA-001. Each certificate is cryptographically anchored with IPFS CIDs.
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerDecidability of Real Polynomial Constraints
Contributor
Apoth3osis Labs
R&D Division
Core insight: the first-order theory of the reals is decidable (Tarski, 1951). This means every quantifier-free system of polynomial inequalities over ℝ has a decision procedure. We can generate machine-checkable certificates of satisfiability or infeasibility — turning real algebraic geometry into a verification tool.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerCylindrical Algebraic Decomposition and Certificate Extraction
Contributor
Apoth3osis Labs
R&D Division
Complete framework: (1) polynomial ring arithmetic over ℝ, (2) sign determination via Sturm chains, (3) cylindrical algebraic decomposition (CAD) for quantifier elimination, (4) certificate extraction — SAT certificates are witness points; UNSAT certificates are Positivstellensatz refutations.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Ontological EngineerLean 4 Formalization — Semi-Algebraic Constraint Solving
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 formalization of quantifier-free real polynomial constraint solving. Polynomial evaluation, sign determination, CAD cell decomposition, and certificate verification. All proved without sorry/admit.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Ontological EngineerSemi-Algebraic Verified Kernel
Contributor
Apoth3osis Labs
R&D Division
All theorems kernel-checked by Lean 4. Guard-no-sorry passes. Standard axioms only.
Builds Upon
MENTAT Contribution Record
BRIDGE
Cross-Level Connection
CONTRIBUTION LEVEL: BRIDGE
Ontological EngineerStandalone Repository + Interactive Examples
Contributor
Apoth3osis Labs
R&D Division
Published as standalone GitHub repository with interactive examples of polynomial constraint solving and certificate verification.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026