Repository navigation
Conversation
…factor Record a byte-identity baseline of every generated Lean certificate on the unmodified code, so the upcoming backend refactor can be proved behaviour-preserving. - tests/lean_golden/corpus.m: 342 Verify -> False items covering the showcase rows, every generator branch, refusal messages, the heuristic engine and oracle queries. - tests/lean_golden/dump.m: dumps the generated Lean fields and the $MessageList message-name sequence for each item. - tests/lean_golden/golden.txt: the recorded baseline. - tests/test_lean_golden.c + CMake target lean_golden_tests: compares a fresh dump with golden.txt (LEAN_GOLDEN_UPDATE=1 rewrites it). Needs no Lean installation.
….6524 Certify becomes a prover-neutral pipeline with Lean as one registered backend. Behaviour is unchanged: the golden corpus (tests/lean_golden, 342 calls) is byte-identical, including every message sequence. - Generators return a neutral IR (neutralGen): the result, the theorem shown to the user and a typed "Obligation" (Identity, PolyIdentities, IdealImplication, RootsComplete with a ClosedFact fallback, ClosedFact, WeightedSOS, KKT, Primality, Induction, HasDerivAt) plus "DomainForm", "Method", "Requires" and, for Integrate claims, "ClaimForm". They contain no Lean text. - LeanBackend.m (new, loaded by Lean.m after EndPackage) holds discovery, LeanVerify and the source check, Method scripts, translation, one Lean encoder per obligation type (leanEncode), the Tier 1 HasDerivAt walk, chunk/footer assembly, runBatch and attribution, the verdict cache, the "Lean" registry entry (leanRun / leanPresent) and the oracle. It opens Lean`Private` itself and creates no Lean` symbol. - Lean.m keeps the usage strings, messages, claim walker, domain rules, generators, the registry ($backends, registerBackend), the pipeline (encodeFor right after generate, postEncode for the Integrate claim form) and the heuristic "Mathilda" backend. certifyItems dispatches to the engine's Run and Present hooks; the summary box reads the backend's Label. - Lean.m: 2393 -> 1599 lines. The test-pinned private names and signatures are kept. Version 0.6524 (src/version.h, lean/lakefile.toml); changelog and the package layout in formal-verification.md and the design note updated.
Certify gains an always-available in-tree engine and engine lists.
- ExactBackend.m (new): Engine -> "Exact" re-checks every certificate kind
with Mathilda's exact rational arithmetic and polynomial Expand, recomputed
from the obligation's statement plus the certificate data (identities with
and without equality hypotheses, polynomial identities incl. surds, ideal
membership, Solve completeness/soundness, matrix facts with an independent
cofactor det, SOS, KKT, Pratt replay, sums via an exponential-polynomial
zero test, D/Together for HasDerivAt). Verdicts are Missing["Exact",
True|False] or Missing["NotChecked"], never True; obj["Checks"] lists each
check; Certify::exactfail on a failed check.
- Engines.m (new): Engine values and lists, Certify::engineopt, the
non-kernel True guard, multi-engine consensus (only a kernel makes the
combined verdict True; Certify::disagree), the multi-engine ProofObject
("Engines", "EngineDetails") and the heuristic engine moved from Lean.m.
- Lean.m: list-aware encodeFor/certifyItems/Format, new messages and usage
text; an Exact-only call makes no Lean encoding. 1593 lines.
- Tests: lean_exact_tests (no Lean), Lean-gated multi-engine cases in
lean_verify_tests, leak gate extended. Golden corpus unchanged.
- Showcase summary gains an Exact column; formal-verification.md (Engines
and consensus), design note, changelog. Version 0.6525.
…; v0.6526
When a kernel engine rejects an item, Certify searches a counterexample
(bounded; "Counterexample" -> Automatic is 2 s, False turns it off). A
witness confirmed by exact arithmetic (in the statement's domain, every
hypothesis true, the conclusion false, every denominator of the claim
nonzero) becomes a Lean theorem not (S) proved by
fun h => absurd (h w...) (by decide +kernel), run in one Lean file per
call. The object gains "Counterexample", "Refuted", "RefutationTheorem"
and "RefutationSource", issues Certify::refuted and displays
"Refuted: {x -> -1}".
New public Refute[claim, opts] (identities, implications of equations,
ForAll / inequalities, Sum == C, Integrate[f, x] == F) returns a
ProofObject of Kind "Refutation". Algebraic witnesses (x -> -2 I) and
claimed antiderivatives are refuted by exact arithmetic only.
Code in src/internal/lean/Refute.m plus "Refute" hooks of the Lean and
Exact backends; generators gain a statement-only mode. Tests:
lean_refute_tests (no Lean) and Lean-gated cases in lean_verify_tests;
the golden corpus is unchanged.
A claim whose certified statement omits the call's Domain / Assumptions (sums, inequalities, implications; only identity claims state them) was refuted without them: Refute[x^2 >= x, Assumptions -> Element[x, Integers]] "refuted" a claim that is true over the integers with x -> 1/2. withAssume adds the options as an "Assume" condition to the refutation problem; the grid, FindInstance and witnessOK require it to hold exactly at the witness, in Refute and in the automatic search after a Certify rejection. The condition is listed in the refutation's TrustedSteps. Refute no longer issues Certify::optignored. Tests: test_domain_assumptions (lean_refute_tests), a Lean-gated sum case with Assumptions -> n > 3 (lean_verify_tests). Golden corpus unchanged.
New public Conjecture[expr, n, opts]: evaluates the held expr exactly at
12 fit and 40 test points, guesses a closed form (Polynomial via
InterpolatingPolynomial, Geometric via an exact Hankel NullSpace
recurrence with rational characteristic roots, Fibonacci, Rational,
Hypergeometric), tests it, and certifies the claim expr == guess as
written (default engines Lean and Exact). Status is Proved (kernel),
Checked (exact re-check only), Refuted or Tested. Conjecture[Sum[k^4,
{k, 1, n}], n] is proved by induction in Lean.
Closed-form sum certificates accept Fibonacci[k + j] / Fibonacci[n + j]:
the Lean source defines a recursive _F on the naturals (trusted step: it
is Mathilda's Fibonacci) and unfolds it in the induction; the Exact
engine rewrites Fibonacci[n + j] linearly in F(n), F(n + 1). Sums without
Fibonacci are byte-identical (golden corpus unchanged).
The option checks move verbatim from Lean.m to Engines.m (line budget).
Tests: lean_conjecture_tests (no Lean), Lean-gated Conjecture cases in
lean_verify_tests, leak gate coverage.
The Lean integration design note now describes the package as built: the pipeline from the neutral IR through the per-backend Encode / Run / Present hooks to consensus and automatic refutation, the six files of src/internal/lean and their load order, a Prover backends section (registry and hook table, trust enforcement, the Exact trust statement, consensus, refutation faithfulness) and a ten-step guide to adding a backend. The follow-up table gains F12-F18. The showcase gains rows 21-29: three-engine consensus with the automatic counterexample, three kernel-checked refutations, three Proved conjectures (Sum k^4, Sum k^2 2^k, Sum Fibonacci[k]^2), a Tested conjecture with no certificate kind, and a row showing that refutations honour Domain and Assumptions. The formal-verification reference lists the refutation keys, the Counterexample option and the new package files; the leak gate runs the new showcase calls with Lean; changelog and the examples README updated.
showcase_output.txt is a fresh run of examples/lean/showcase.m (exit 0, "All rows as expected") on the committed package, with the new consensus, refutation, conjecture and Domain/Assumptions rows; the examples README records the run's wall time and machine load.
- A held Sum in an Equal whose iterator the closed-form sum generator does
not take ({k, 1, n + 1}, {k, 1, 2 n}, {k, n, 2 n}, ...) no longer falls to
the identity generator, which evaluated both sides and certified
Mathilda's own Sum output against itself: Certify::nocert, so Conjecture
reports "Tested" and Refute gives no spurious witness.
- "Status", "Refuted", "Counterexample" and "RefutationTheorem" are gated by
authentication like "Verified".
- Generic ordered-field / char-0 statements pick a type variable (K, K1,
...) that the claim does not use; the refutation's named argument follows
it, so a claim variable K is no longer captured.
- Refute's Domain/Assumptions restriction splits only a top-level And.
- Regression tests in lean_conjecture, lean_refute and lean_verify (Lean-
gated); golden corpus unchanged.
msollami
marked this pull request as ready for review
November 12, 2026 00:45
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Stacked on #134.
Certifystops being Lean-only: generators now emit a prover-neutralobligation, and backends registered by name encode, run and present it. On top of that
registry this PR adds a second always-available engine (
"Exact"), multi-engine consensus,kernel-checked refutations with a counterexample search (
Refute, and automatically after arejection), and an experiment -> guess -> test -> certify loop (
Conjecture). Every Leanartefact that existed before is byte-identical (golden corpus of 342 records, recorded before
the refactor and unchanged through every commit).
Trust is unchanged: only a kernel can make
"Verified"True. The pipeline rewrites aTruefrom any backend whose"Trust"is not"Kernel"toMissing[name, True].Changes
712e7fb7, after the golden corpusd1ea1792). Generators return a typed"Obligation"(Identity, PolyIdentities,IdealImplication, RootsComplete, ClosedFact, WeightedSOS, KKT, Primality, Induction,
HasDerivAt) plus a
"DomainForm";registerBackendvalidates each backend's hooks(
"Encode","Run","Present","Label", optional"TrustedSteps","Options","Refute").Lean.mis split: the neutral core stays, the Lean backend moves toLeanBackend.m. No behaviour change.12ba66de).Engine -> "Exact"re-checks eachobligation with Mathilda's exact arithmetic and
Expand, recomputed from the statement,never from the generator's own pre-check. It reports
Missing["Exact", True | False]orMissing["NotChecked"], neverTrue: it is an exact re-check by the system that producedthe certificate, not a proof.
"Engine"may be a list: every engine runs,Falsefromany non-heuristic engine wins,
Trueneeds every kernel to agree,Certify::disagreeflags a kernel that disagrees with another engine. New keys
"Engines","EngineDetails".New file
Engines.m.Refute(3e569338, follow-up93447878). After akernel rejection a bounded deterministic search (exact grid, then
FindInstance) looks fora witness; Lean then proves
¬ Sfor the certified statement S(
fun h => absurd (h w…) (by decide +kernel), the generic type variable instantiated atRat).Faithfulness rule: the witness must lie in S's quantifier domain, satisfy its hypotheses,
falsify its conclusion, keep every denominator of the claim nonzero, and satisfy the
call's
Domain/Assumptionswhen S omits them; all checked by exact arithmetic,FindInstance's domain argument is not trusted. Algebraic witnesses (-2 I) giveexact-only refutations.
Refute[claim]exposes this directly; new keys"Counterexample","Refuted","RefutationTheorem","RefutationSource". New fileRefute.m.Conjectureand Fibonacci sums (a78f749e).Conjecture[expr, n]fits 12exact values with polynomial, linear-recurrence, Fibonacci, rational and hypergeometric
guessers, tests the guess on 40 more, and certifies
expr == guessas written. Status"Proved"(kernel),"Checked"(exact only),"Refuted"or"Tested"(no certificatekind). Closed-form sums accept
Fibonacci[k + j], proved through a Lean definition of F(one trusted step: it is Mathilda's
Fibonacci, checked at n = 0..29). New fileConjecture.m.55f43906). An adversarial review found that aSumwhose iterator is not{k, a, n}(e.g.{k, 1, n - 2}) fell through to theidentity generator, which evaluated both sides, so Lean checked Mathilda's own
Sumoutput against itself:
Conjecturecould report "Proved" for a claim false at n = 0, andRefutecould report witnesses where the claim holds. Such sums now get no certificate(
Certify::nocert;Conjecturereports "Tested"). This also closes the same gap in plainCertifyinherited from the base. Every verdict-bearing key ("Verified","Status","Refuted","Counterexample","RefutationTheorem") is now authenticated, so a tamperedobject reads
Missing["Unauthenticated"]. The generic type variable is renamed (K1, …)when the user's statement uses
K;Assumptionssplit only at the top-levelAnd.Regression tests for each finding, including Lean-gated ones.
docs/design/lean_integration.md: thepipeline, the six package files and their load order, a Prover backends section (hook
table, trust enforcement, consensus, refutation faithfulness) and a ten-step "Adding a
backend" guide; follow-ups F12-F18. Formal-verification reference, changelog, examples
README, leak gate updated. Showcase rows 21-29:
the counterexample
x -> -1refuted by the kernel;Refute: a wrong cube expansion, an inequality over every ordered field, thefreshman's dream over the integers (each kernel-checked);
Conjecture, Proved:Sum[k^4],Sum[k^2 2^k],Sum[Fibonacci[k]^2];Conjecture[Sum[Binomial[n, k]^2, …]]:Binomial[2 n, n], Tested (WZ is a follow-up);x^2 >= xwithAssumptions -> Element[x, Integers]: neither proved nor refuted,while
x -> 1/2refutes it without the assumption.Testing
ctest -LE nightly -j6at HEAD (v0.6528, clean tree): 100% tests passed, 0 failed out of650 (647 before the PR, +
lean_exact_tests,lean_refute_tests,lean_conjecture_tests);lean_mathlib_testsandlean_check_tokens_mathlibSkipped (no Mathlib project configured), as on the base.ctest -R 'lean_|context_tests'with Lean 4.35.0-rc3: all pass apart from the two Mathlibskips (
lean_verify_tests268 s under load);lean_verify_testscovers multi-engine runs, automatic refutations,
Refuteand Proved conjectures with thereal kernel.
MATHILDA_LEAN=/nonexistent ctest -R 'lean_(golden|certify|exact|refute|conjecture)':5/5 at v0.6527 (everything except the Lean-gated suites runs without Lean).
lean_golden_testspasses,tests/lean_golden/golden.txtunchanged sinced1ea1792(342 records: every generated statement, proof, source and message sequence).sh tests/scripts/lean_leakcheck.sh ./Mathilda: 0 leaks for 0 total leaked bytes, real Lean runsincluded (Exact, consensus, searches,
Refute,Conjecture, Fibonacci sums)../Mathilda -file examples/lean/showcase.m: exit 0, "All rows as expected", 118 sin total at load average 13-35 (64 s at load 6-10);
examples/lean/showcase_output.txtregenerated from that run.this work): accepted
Certifyabout 1.8 s per call; rejection plus kernel-checkedrefutation 2.3-2.4 s (0.6 s with
"Counterexample" -> False); each new showcase row1.7-2.4 s;
Conjecturewith a Proved result 1.9-2.4 s. Startup cost of the splitpackage: +1.1 ms median.
"DomainForm" -> "Real"),WZ / Zeilberger certificates, public
FindLinearRecurrence/FindSequenceFunction,best-constant conjectures, Mathlib refutations with surd witnesses, a
mathilda?Leantactic, an idle-machine timing baseline.
JIRA Ticket
N/A