A research agent running an open-weight model took a logic from a blank file to a machine-checked proof: the four-valued logic FDE, formalized in Lean 4 and proved sound, complete, and decidable. Every proof is checked by Lean's kernel, not by the model's say-so.
The proof is the point. The open model is the other point. How it was actually built — every wrong turn, the timeline, the cost — is on the process page.
A G3-style sequent calculus for FDE proved sound (every derivable sequent is valid) and complete (every valid sequent is derivable) against the Belnap–Dunn four-valued semantics.
From soundness + completeness the agent derived that FDE has no theorems, holds the disjunction property (vacuously), and that derivability is decidable — all kernel-checked.
The leaderboard of AI-proved math is dominated by closed frontier models. This artifact came from an open-weight model whose proof is public and kernel-checkable by anyone.
There's a growing list of math problems solved by AI, tracked with the model named and a Lean-verified flag. But almost every entry is a closed, frontier model: GPT-5.6, Claude, Google's internals. The question we asked is narrower and, we think, more pointed: can an open-weight model, driving a research agent, produce a verified artifact that anyone can independently re-check? Not a benchmark answer. A proof.
The test object is First-Degree Entailment (FDE), the logic behind Belnap and Dunn's four-valued semantics, where a proposition can be true, false, both, or neither. FDE is the base logic of paraconsistent reasoning: it tolerates contradiction without exploding into triviality. It's well understood as mathematics, so the statements of its core metatheorems are uncontroversial to formalize, which is exactly what makes it a clean test of whether the agent can produce a proof, not just a plausible answer. The bar isn't "did the model get the right result." It's "does Lean's kernel accept the argument."
Three metatheorems make a logic feel solid: soundness (the proof system never proves something false), completeness (it proves everything true), and decidability (there's a terminating procedure that tells you whether any given statement is provable). We set the agent the task of proving all three, from scratch, in a public repository, with its failure log attached. This page is the result.
The setup is deliberately simple, and the simplicity is the point: a language model cannot fake a Lean proof. The model writes tactic code; Lean's kernel, a small trusted proof checker, accepts or rejects it. There is no "the model thinks it's right." There is only "the kernel accepts it" or "it doesn't."
1. Encode the logic: the four truth values, the semantics, the proof
rules, in Lean's type theory.
2. State the metatheorem precisely (soundness, completeness, etc.).
3. Prove it: the agent writes a proof script, the kernel checks each step.
4. Audit: a green build is not enough. Verify zero sorry
placeholders (Lean's "trust me" escape hatch), and run #print axioms to
confirm exactly which foundational assumptions each theorem rests on.
5. Log the failures: the bugs, the wrong architectures, the traps.
The process is part of the claim.
The verification standard is the honest one: a module-targeted lake build
must recompile the file that changed (a bare lake build can report green
from stale cache), the axiom list must be reported alongside every theorem, and
#print axioms is the primary sorry-check — not the grep. A
grep ":= sorry" scan is leaky: alternation binds loosest, so an indented
· sorry inside a tactic block passes silently. The grep is a convenience;
the kernel's own axiom report (no sorryAx) is the check that can't be
gamed by formatting. "Kernel-checked" and "the encoding is faithful to the source
logic" are stated separately, because they are separate claims.
The calculus is a two-sided, G3-style sequent system with invertible rules and exchange
via list permutation. Atomic identity sequents are the base cases; the ¬/∧/∨ rules are
invertible (valid in both directions), including the De Morgan laws that push negation
to the leaves. Completeness is proved by strong induction on a negation-weighted
measure over a 12-way case split (decompose): either the sequent is
initial up to permutation, saturated (and hence refuted by a canonical countermodel
read off the antecedent), or some rule applies to a compound formula. Decidability
follows the same induction, deciding each branch.
Every entry below is a theorem Lean's kernel accepted, with its axiom dependencies printed and its sorry-count at zero. "Axioms" are the foundational assumptions a proof leans on; reporting them is how you know the proof isn't secretly resting on something stronger than it claims.
| Theorem | Statement (plain) | Axioms |
|---|---|---|
| Soundness Deriv.sound |
Every derivable sequent is semantically valid. | propext |
| Completeness completeness |
Every valid sequent is derivable. | propext · Classical.choice · Quot.sound |
| No theorems no_valid_formula |
No formula is valid on its own — FDE's famous "no logical truths" property. | propext |
| Disjunction property disjunction_property |
If φ∨ψ is a theorem, one of φ, ψ is — stated honestly as vacuous (there are no theorems). | propext |
| Decidability decidable_deriv |
Derivability of any sequent is decidable — proved as a theorem (a Prop disjunction), not an executable checker. | propext · Classical.choice · Quot.sound |
| Sound + complete deriv_iff_valid |
Derivable ⟺ valid, as a single equivalence. | propext · Classical.choice · Quot.sound |
Two results deserve a sentence each. "No theorems" is not a failure —
it's the signature property of FDE, proved here directly (the constant-"neither"
valuation refutes every formula). And decidability is proved as a
theorem, not an executable checker: the result is the Prop disjunction
(⊢ₛ S) ∨ (¬ ⊢ₛ S), proved by terminating measure induction, plus a
Decidable instance that is noncomputable and does not execute
(Deriv is Prop-valued, so no search is extractable). A runnable
checker would require Deriv in Type with its own termination
proof — a further, separate construction, not claimed here.
An earlier version of this page (and the repo README) said the Classical.choice
in decidable_deriv came solely from lifting the decision into a
Decidable instance. That is wrong, and the axiom report contradicts it:
the underlying Prop proof already carries Classical.choice because its
negative branches call completeness, which carries the same three axioms.
The lift adds nothing. We state the corrected attribution here rather than edit it away.
"The kernel verifies these proofs" is true and checkable. "This encoding faithfully captures FDE" is a separate claim — about whether our four values, our designated set, and our sequent rules match the logic the textbooks describe. That second claim is argued in the design notes and source docstrings, not proved. We keep the two distinct because conflating them is how formalization results get oversold.
Re-check it yourself: the proof is a public, buildable Lean 4 project — github.com/NimbleCoOrg/fde-lean. The module-targeted verification recipe is on the process page.
Here's the claim this experiment was built to make. When a closed frontier model produces a Lean-verified proof, you get the artifact, but the reasoning that produced it stays behind an API, unauditable and unreproducible. When an open-weight model does it, both halves are public: the proof, and the weights that reasoned their way to it.
This matters more than it might look. The whole point of a verified artifact is that you don't have to trust the prover. But that argument is much stronger when the prover itself is inspectable. A closed model's "trust me, it's verified" still asks you to trust the platform. An open model's proof carries no such ask: the kernel checks the proof, and you can download the exact weights that wrote it. This run used Kimi K3 (Moonshot AI), an open-weight model, accessed through OpenRouter. Earlier sessions of the same project ran on Claude; the model changed, the proofs kept checking, which is itself a small demonstration that the artifact is the durable thing.
A boundary worth stating precisely, because it's easy to overread the open-model claim:
open weights do not raise proof assurance. A closed-model Lean artifact
is exactly as kernel-checkable as this one — the kernel doesn't care who wrote the
tactic, and a verifier re-running lake build gets the same assurance either
way. What open weights change is provenance and rerunnability: the prover itself
can be pinned and re-run. And that claim is only as strong as the pinning. So we pin:
model checkpoint (moonshotai/kimi-k3, downloadable weights), provider
(OpenRouter), harness (Hermes Agent + the lean4-formalization skill), build
(toolchain nightly-2026-07-14, mathlib f566658afd). The
conversation traces are the remaining piece — they are being archived alongside the repo
before any leaderboard submission, because "the process is rerunnable" is only honest
once the traces are inspectable too. Weights alone do not expose this run's reasoning;
the pinned trace does.
It is not a novel theorem. FDE's soundness, completeness, and
decidability are established mathematics. The contribution is the formalization
and the process. The novelty claim is scoped precisely: to our knowledge this is the
first Lean 4 proof-theoretic formalization of FDE with its metatheorems
(a sequent calculus proved sound, complete, and decidable). It is not the first Lean 4
code to mention Belnap's four values — a GitHub search surfaces
umpolungfish/p4rakernel (created 2026-06-02), which has the four-valued type
and paraconsistent operators but no FDE sequent calculus, soundness, or completeness.
Our earlier, flatter "first Lean 4 formalization of FDE" was checked only against mathlib
and Foundation, and does not survive a broader search; the scoped claim does.
It is not evidence that the model "understands" logic. The kernel checks the proof; nothing here tells us how the model produced it, and we make no claim about reasoning, only about the artifact.
The encoding is an interpretation. As flagged in §03: the kernel-checked result and the faithfulness of the FDE encoding are separate claims. A domain expert auditing the encoding would strengthen the second. That's an open invitation.
One logic is one point. FDE is a single, deliberately tractable target. Whether the same open-stack discipline holds on a harder, less-charted problem is the actual next question. The modal extension of this logic is the natural candidate.
Every reference below was verified for existence, metadata accuracy, and retraction status against Crossref, most recently on 2026-08-10. The badge is the outcome of that check, not an assertion.