Gödel's and Scott's Variants of the Ontological Argument in Lean 4
cs.LO · cs.AI
Quick verdict
Machine-checked Lean 4 port of Benzmüller–Scott's Isabelle/HOL dataset (30 theories); sound, honest; novelty: per-theorem modal-logic dependency bounds.
Summary
This paper reports a structure-preserving port to Lean 4 of the Isabelle/HOL dataset accompanying Benzmüller and Scott's study of Gödel's and Scott's modal ontological arguments. Thirty Lean modules mirror thirty Isabelle theories, preserving names, declaration order and section structure; a shipped comparison tool certifies all 548 statements identical, backed by live re-parsing checks (417 Isabelle statements, 399 Lean declarations). Everything the original proves is re-proved, including the inconsistency of Gödel's 1970 axioms, the two repaired Gödel variants, Scott's variant, modal collapse, monotheism and the ultrafilter property; five statements the original left unreplayed — one of them postulated there — are now proved with explicit terms, since Lean lacks sledgehammer. The 45 remaining statements are exactly the 35 nitpick-refuted and 10 open ones, kept as anonymous sorrys on which nothing depends (#print axioms confirms no sorryAx dependency). The main new contribution is per-theorem dependency accounting (Table 4): Scott's necessary existence and modal collapse need only symmetry (KB); the essence and monotheism lemmas, positivity of the universal property and possible existence of a God-like being need no frame condition; the 1970 inconsistency needs none but iNonempty. Limitations: countermodels are documented, not re-run (Lean has no model finder); Table 4 gives upper bounds only, calibrated against Isabelle citations; definitions escape the parse-agreement checks. Sources ship as a self-contained lake package (Lean 4.33.1).
Review complete
Assessment at a glance
4
risk flags identified
● high 0
● medium 1
● low 3
5 strengths · 5 weaknesses · 5 author questions
AI text signal = Binoculars zero-shot detector score over 20 sampled passages (Fast-DetectGPT co-reported) — absence does not prove human authorship, and a flag does not imply misconduct.
Levels reflect verification complexity — not a quality score. Evolve never rates your paper.
Key claims under review
- A complete, structure-preserving Lean 4 port of the 30-theory Isabelle/HOL dataset exists, with all 548 statements machine-verified identical to the originals by a shipped comparison tool plus live re-parse checks on both sides.
- Everything the original proves is re-proved in Lean 4, including five previously unreplayed statements, one of which (Th4 of Gödel variant 3) the original had postulated as an axiom.
- The 45 unproved statements are exactly the 35 nitpick-refuted and 10 open ones of the original, kept as anonymous sorrys on which no named result depends (no sorryAx in any #print axioms output).
- Per-theorem #print axioms accounting (Table 4) shows Scott's necessary existence and modal collapse require only symmetry (KB), while Th1/T1/T2, Monotheism, Th4, and the 1970 inconsistency need no frame condition at all — the inconsistency consuming only iNonempty.
- The routine, idea-free translatability of the whole dataset evidences that the LogiKEy embedding methodology transfers to Lean 4.
Strengths
Layered verification beyond the kernel
Section 3 checks not only that proofs type-check but that statements match: AST comparison certifies 548/548 statements identical, guarded by live re-parse checks on both sides (417 reparenthesised Isabelle formulas validated by generated Isabelle theories; 399 Lean declarations equated via `with_reducible rfl` across 25 files), plus mutation testing showing the tool detects dropped connectives, moved parentheses, identified variables, and a dropped box.
Exemplary honesty about what is and is not verified
Nitpick results are explicitly labeled 'documentation, not verification' (72 invocations recorded verbatim); Table 4 is stated to be upper bounds 'not a minimum'; the calibration blind spot (inheriting slack from Isabelle citations) and the object-language vs. full-function-semantics gap are both flagged in Section 5.
Genuinely new logical information extracted
Complete reproducibility package
Five previously unreplayed statements closed
Weaknesses
Negative results are not re-verified in Lean
Dependency table is upper bounds only
Definitions escape the live parse-agreement checks
Incremental novelty
Heavy AI assistance in port and drafting
Full Review Report
$1.99 · one-timeUnlock the complete preliminary analysis Evolve produced for this paper.
Report preview
Scope & Claims
This is a proof-engineering paper: a complete port to Lean 4 of the Isabelle/HOL dataset from Benzmüller & Scott's Monatshefte study (ref [3]), organized as 30 Lean modules mirroring 30 Isabelle theories. The claims are deliberately modest and precisely bounded: (1) the port is structure-preserving — names, declaration order and section structure retained; (2) a shipped comparison tool certifies all 548 statements identical; (3) everything the original proves is re-proved, plus five statements left unreplayed there, one of which (Th4 of Gödel variant 3) the original had postulated as an axiom; (4) the 45 unproved statements are exactly the 35 nitpick-refuted and 10 open ones of [3], kept as anonymous `sorry`s; (5) `#print axioms` yields a per-theorem dependency table (Table 4) bounding the modal logic each result requires. The paper explicitly disclaims new philosophical analysis; the novelty is the Lean dataset plus the dependency accounting.
The remaining sections cover Methodology Assessment, Statistical Evidence, Results & Reproducibility, Limitations & Risks, and Verdict & Recommendations.
- All 5 strengths & 5 weaknesses, analyzed in detail
- 4 risk flags with severity, section & reviewer questions
- Methods & statistical evidence assessment
- 5 questions a peer reviewer would ask
- Full six-dimension evaluation report & recommendations
One-time purchase · this paper only
One-time purchase, this paper only. AI-generated preliminary analysis — not peer review.
Frequently asked questions
Does this paper prove that God exists?
No. It re-mechanizes existing formal developments of Gödel's and Scott's ontological arguments in a different proof assistant. All results are conditional on formal axioms that are philosophically contested; notably, the port re-proves that Gödel's original 1970 axioms are outright inconsistent, and Scott's variant yields 'modal collapse' (every truth is necessary), which is widely taken as a reason to reject those axioms rather than as a proof of God.
What is new compared to the earlier Isabelle/HOL work on Gödel's ontological argument?
Two things: a complete Lean 4 port of all 30 theories of the Benzmüller–Scott dataset with explicit proof terms (Lean has no sledgehammer automation), and a per-theorem dependency table (Table 4) showing which modal frame conditions each result consumes — e.g., Scott's necessary-existence theorem and modal collapse need only symmetry of the accessibility relation (logic KB), while several lemmas hold with no frame condition at all.
Why do 45 statements in the development remain unproved?
They correspond exactly to the 35 statements the original Isabelle/HOL work refuted using nitpick countermodels and the 10 it left genuinely open (e.g., Th3 of the S4 restrictions). In the Lean port they are anonymous 'sorry' placeholders on which nothing downstream depends — verified via #print axioms — so no proved result relies on them.
How can I reproduce or verify this work?
Download the paper's ancillary files, unpack them, and run 'lake build' with Lean 4.33.1: all 30 modules type-check with no dependencies beyond Lean's core. The package also includes the statement-comparison tool, the script that generates the dependency table with its full output, and Isabelle check sessions with their build log.
About this review
This is an AI-generated preliminary review by Evolve.Pub, produced from the openly available text of the paper. It is not peer review and does not represent the authors' views. The canonical record of the paper is at the publisher link above.
- Two passages were elided in text extraction (parts of Section 4's end and Section 5's beginning); Table 4 and the surrounding dependency analysis are present, so core judgments are unaffected.
- The review is based on the extracted text only; the ancillary source files were not inspected, so audit counts (548, 566, 417, 399, 72, 45) are taken as reported.
- No original figures exist beyond Table 1 (notation) and the source appendix; nothing visual was lost in extraction.
- The paper's comparison-tool guarantees depend on the accompanying AFP sources of [3], which were not independently checked here.
Go deeper on this paper
Wrote a paper? Stress-test it before reviewers do.
Upload your manuscript for the same structured scrutiny — reasoning, statistics, evidence, figures, and reproducibility.