|
| 1 | +# LLM Proof Trust Statement — 2026-03-30 |
| 2 | + |
| 3 | +## Context |
| 4 | + |
| 5 | +This note responds to the question: *“How much can you trust proofs proposed by large language models, and what signals matter when those proofs are offered in a conference or publication?”* The short answer is: LLMs can help generate ideas or structure for proofs, but the only proof that counts is one that has survived a machine-checker, so we treat every LLM-contributed argument as a draft that still needs full mechanisation. |
| 6 | + |
| 7 | +## Trust Boundaries |
| 8 | + |
| 9 | +1. **Human-in-the-loop discovery**: LLMs can suggest definitions, lemmas, or proof structure, but they do not know the current codebase state the way a domain expert does. Their outputs are statistically likely but not guaranteed to be correct. We therefore treat their contributions as “propositional sketches” that only become evidence once formalised. |
| 10 | + |
| 11 | +2. **Mechanised verification requirement**: Every claim that reaches a conference or software release must be checked by a legitimate proof assistant (Idris2, Lean 4, Agda, Coq, or a specialist system). The checklist is: (a) the LLM proposal has been ported into the target language; (b) the body compiles/executes with `%default total` (or equivalent); (c) there are zero `believe_me`, `sorry`, `postulate`, or placeholder gaps in the proof tree; (d) CI reproduces the result cleanly. Without those steps, the claim remains an *informal idea*, not a formal proof. |
| 12 | + |
| 13 | +3. **Publication posture**: If we submit a paper or talk and mention “LLM-assisted proof work,” make it clear that the human team controlled the mecanisation and the proof assistant produced the final acceptance. Audiences expect that a “LLM-enabled” proof was vetted with a proof checker. If they ask “did you run it through Idris/Lean/Agda?” the honest answer is “yes, and here is the proof script and log.” Saying “an LLM or Claude wrote the proof” without the machine-checked artefact invites skepticism; reviewers will look for the actual proofs, not the chat transcript. |
| 14 | + |
| 15 | +4. **Community credibility**: Presenting an LLM-assisted proof without the mechanised artefact is a reputational risk. Even if the idea is sound, the community will remain hesitant until they can rerun it themselves. In contrast, showing the mechanised artefact—annotated, tested, and reproducible—signals that we treated the LLM output with the same rigor as any other contribution. |
| 16 | + |
| 17 | +## Actionable Notes |
| 18 | + |
| 19 | +* Always store the mechanised proof file under version control, with the proof assistant command needed to produce it documented in the repo. |
| 20 | +* Log the proof assistant version and command line so reviewers can reproduce the result. If the proof depends on Idris2, record `idris2 --check Proof.idr`; if Lean 4, record `lean --make theorem.lean`. |
| 21 | +* When a paper cites our proof, include the reference path (e.g., `proofs/Idris/TypeLL/Totality.idr`) and the proof assistant output (CI logs or local run). That way the reviewer can confirm the evidence themselves, independent of the LLM conversation. |
| 22 | +* If a claim is still at the “LLM sketch” stage, label it clearly as *proposed* or *conjectured* and do not elevate it to “proven”, “verified”, or “formal” in any README, paper, or release note. |
| 23 | + |
| 24 | +## Summary |
| 25 | + |
| 26 | +LLMs can help brainstorm proofs, but the only trust we extend is to proofs that have been mechanised, type/totality-checked, and reproduced by our CI. Mentioning LLMs in a paper should come with the disclaimer that the final artefact was verified by a theorem prover and that the LLM’s role was limited to the exploratory phase. Without that verification, reviewers will treat the output as low-trust research notes, and our release-pre-flight gate will not clear the claim. |
0 commit comments