{"id":"5fc46d16-d19f-474b-a1e6-379e0d49a47e","arxiv_id":"2608.08643","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A Lean 4 and Mathlib file formalizes every definition, result, and experimental table row of the primes-are-supernatural conjecture paper, with no sorry, leaving the conjecture itself as an open named proposition.","lead":"This paper reports a complete Lean 4 formalization of an earlier manuscript that conjectures no non-constant function built from addition, multiplication, and exponentiation maps every positive integer to a prime. The value is that the conjecture and its surrounding theory now exist as a named, kernel-checked target for automated and human theorem provers.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Central claim hinges on an unpinned, unarchived repository; the paper's own elided snippets cannot certify the no-sorry/exhaustive formalization.","rationale":"The reader's weakest_assumption identifies the same load-bearing concern: the formalization claim depends on an unpinned, externally hosted file. I examined the printed Lean snippets for internal soundness and found no mathematical flaw: the elevation structure axioms match [3, Definition 1.1]; the word encoding and IsNatural are proved equivalent; the proposition, lemmas, and remarks are stated correctly; Proposition 3.1 uses the needed composition lemma; the extended Knuth/factorial/sub class is coherent; and the table theorems and Lucas certificates are plausible. The concern is therefore not 'the proof is wrong' but 'the claim that this is the checked file is unsubstantiated as printed.' The paper itself states that the file carries no comments and is the sole documentation, yet omits a hash and several proof bodies. Because every declaration can be checked by running Lean, this is exactly the kind of issue a CONDITIONAL verdict should carry: the mathematical content is credible, but the completeness/no-sorry claim should not be treated as established until a reproducible build and declaration-level audit are supplied. I would not escalate to REJECT or UNVERDICTED, since the failure mode is an unpinned artifact rather than an identified inconsistency.","tokens_in":857,"tokens_out":901,"duration_ms":216178,"concrete_test":"Obtain a fixed commit hash or release archive of github.com/rndmx/SPCL; in a clean environment with Lean v4.32.2 and the corresponding Mathlib toolchain, run `lake build`. Then run an automated audit that `#check`s every declaration named in Section 11, confirms the 89 table theorems and 16 Pratt certificates are present, and runs `#print axioms` on each theorem to verify no `sorry` and no axioms beyond Mathlib's standard three. If the build succeeds and the audit matches Section 11 exactly, the reproducibility concern is resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's strongest claim is that SPCL.lean is a complete, sorry-free Lean 4 formalization of [3]. That claim is not checkable from the manuscript alone. Section 1 gives only a URL (github.com/rndmx/SPCL) with no commit hash or release archive; Section 2 asserts 'lake build checks everything' and 'sorry-free' without a build log; and the displayed code is explicitly partial (§3 omits 'the seven axioms' proofs, §4 omits the mul/elev cases, and several proofs end with '-- ...'). The Section 11 correspondence table is author-written, not machine-generated, so it does not itself certify that each printed declaration is exactly the declaration in the checked file. If the repository has changed, or if any printed snippet diverges from the file, the completeness and no-sorry claims cannot be confirmed or refuted from the paper. The mathematics shown is coherent, so the concern is about auditability of the artifact, not about the correctness of the formalized statements.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper reports a Lean 4 formalization, in a single file SPCL.lean, of the author's earlier conjecture-oriented paper \"Conjecture: the set of prime numbers is supernatural.\" It claims exhaustive machine-checked coverage of definitions, examples, remarks, numbered results, and experimental tables, with no `sorry`, and it presents selected declaration listings, discusses encoding choices, and gives a correspondence table. It also formalizes an extended class with Knuth arrows, factorial, and truncated subtraction, states an extended conjecture as an unproved `Prop`, and describes Pratt/Lucas certificates for the large primality conjuncts in the experimental tables.","tokens_in":14753,"tokens_out":6117,"duration_ms":62315,"significance":"If the formalization is complete and the repository compiles as claimed, the paper is a useful artifact: it turns an open conjecture into a named, kernel-checked proposition; it verifies all 89 experimental table rows, including large primality claims; and it makes precise some informal proof steps in the source paper, notably the composition-closure lemma needed for Proposition 3.1. The use of external computation only for certificate search, with all certificate checks performed by the kernel, is a sound and reproducible pattern. The main limitation is that the central claim of exhaustive, sorry-free coverage is not independently auditable from the manuscript alone.","major_comments":[{"comment":"The central claim of a complete, sorry-free formalization cannot be checked from this manuscript. Section 1 gives only a bare URL for SPCL.lean, and Section 2 asserts that `lake build` succeeds and that the file is sorry-free, but no commit hash, archive, build log, or `#print axioms` transcript is supplied. Because the displayed snippets are explicitly partial (§3 omits the seven axiom proofs, §4 omits the `mul` and `elev` cases, and several proofs end with `-- ...`), the reader cannot verify that the printed declarations are exactly the declarations in the checked file. Please pin the exact commit or provide a release archive, and include the build output and the relevant `#print axioms` output for the stated toolchain, so that the completeness and no-sorry claims become reproducible.","section":"§1, §2"},{"comment":"The correspondence table is author-written rather than machine-generated, and it cannot by itself certify that every claim in the paper has a proof in the repository. The table is valuable as documentation, but the paper should either provide a machine-checkable coverage certificate linking each printed declaration to a name in the file, or state clearly that the table is a human-readable summary. In addition, the table records an explicit gap: the row for [3, §4, question (ii)] says \"not a determinate proposition as printed; not encoded.\" If the abstract's phrase \"every ... numbered result\" includes that question, the coverage claim needs to be qualified; if it does not, the boundary should be stated in the abstract and in Section 1.","section":"§11"},{"comment":"The paper's description of the proof of the large table rows is plausible but not fully demonstrated: Section 10 says the heavy conjuncts are proved by Lucas certificates, with `lucasCert` converting an explicit factorization into Mathlib's `lucas_primality`, but the only fully displayed certificate is for the single prime `18446744073709551709`. The paper should state precisely how many certificate theorems are used, which table rows depend on them, and how the external certificate data is represented and checked, so that the claim that all certificate data is untrusted and kernel-verified can be audited.","section":"§2, §10"}],"minor_comments":[{"comment":"The prose statement of Proposition 2.2(ii) writes \"f(n)=a n + b\", while the formal statement `prop_2_2_ii` and the surrounding proof use `a ^ (n :N) + b`; please correct the displayed formula in the prose.","section":"§8"},{"comment":"The theorem `isNatural_of_mem_word` is presented in two slightly different forms: the earlier declaration has `{σ : Word} {f : N+ → N+}` before the colon, while the proof block writes `: ∀ {σ : Word} {f : N+ → N+}, ...`. Please align the two displays.","section":"§4"},{"comment":"The correspondence table lists `Question_i` as \"stated (open)\", but no declaration text or section of the paper displays this Lean statement; please include the declaration or a clear pointer to it.","section":"§11"},{"comment":"The category instance `ElevCat` proves the category laws by `rfl`, so it would be helpful to state explicitly whether the bundled `ElevationHom` structure uses proof irrelevance or definitional equality in a way that makes the three laws hold definitionally; without that explanation, a reader may be surprised that `id_comp`, `comp_id`, and `assoc` close by `rfl`.","section":"§3"}],"recommendation":"major_revision","confidential_remarks":"The paper's value depends entirely on the repository SPCL.lean being reproducible and exactly matching the printed declarations. The lack of a commit hash and build log is the main obstacle. I would ask the editor to make the revision conditional on a pinned commit or archive, a build log, and a clear statement of which Mathlib commit was used. The prose is otherwise coherent and the formalization choices are sensible."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this is a Lean 4 formalization of a niche conjecture paper, and the artifact is genuinely useful even though no new mathematics is proved. The main value is that the conjecture becomes a precise named Prop, and every proved claim in the source paper is formally verified without sorrys. I read the displayed code carefully; it is coherent, the encodings are sensible (particularly the word vs. inductive closure equivalence and the shift-composition lemma for Proposition 3.1), and the Lucas-certificate handling of the large primality checks is a nice engineering touch. The extension of Remark 3.4 with Knuth arrows, factorial, and truncated subtraction is real new content, and the embedding theorem shows it really extends the original class.\n\nSoft spots, in proportion: the paper's strongest claims—'complete,' 'sorry-free,' 'exhaustive'—are not verifiable from the preprint alone. There is no commit hash or archived copy of the repository, no build log, and several proof snippets are explicitly elided. The Section 11 correspondence table is author-written, not machine-generated. If the repo has drifted from the printed declarations, the completeness claim cannot be confirmed or refuted. This is a reproducibility gap, not a mathematical flaw: the statements shown are internally consistent, and I don't find a problem in the formalization design. The stress-test note is right that the central claim rests on an unpinned artifact.\n\nThe citation pattern is fine. The mathematics comes from the author's own 2025 paper, but that is the object being formalized; the formalization itself and the extended class are new. Self-citation here is appropriate.\n\nWho should read it: anyone interested in formal mathematics pipelines, AI theorem proving benchmarks, or using Lean to make open conjectures into checkable targets. It would serve as a good case study. I would send it to peer review, but I would make acceptance conditional on the author providing a pinned artifact. Ask for a commit hash or a tarball, and ideally a CI build log. Without that, the 'no sorry / complete' claim is just a promise.","headline":"A serious Lean formalization of a niche conjecture paper, with real new content in the extended class, but the 'complete no-sorry' claim currently rests on an unpinned repository.","tokens_in":15286,"tokens_out":2328,"would_cite":true,"duration_ms":23614,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B35","68V20"],"pacs":[],"model":"deepseek-v4-flash","headline":"The primes-are-supernatural conjecture is now a Lean proposition.","keywords":["Lean 4","Mathlib","formal proof","prime numbers","natural functions","conjecture formalization","elevation structures","kernel-checked proofs"],"falsifier":"Compile the companion source file with the stated theorem prover and library versions, then inspect the named Conjecture_2_1, the correspondence-table theorems, and the #print axioms output; if any listed theorem is missing, contains sorryAx, or uses an undeclared axiom, the completeness and no-sorry claims are false.","tokens_in":14357,"feed_emoji":"🔢","tokens_out":9088,"duration_ms":82203,"temperature":0.7,"pith_summary":"The paper claims to give a complete formalization, in the Lean 4 theorem prover over its Mathlib library, of the conjecture that no non-constant function built from the identity and constants by finitely many additions, multiplications, and exponentiations maps every positive integer to a prime. Every definition, example, remark, numbered result, and experimental table row of the source paper is said to have a machine-checked counterpart, with no sorry gaps. The conjecture itself is recorded as a named, unproved Lean proposition, so that a future proof, whether found by a human or by an automated reasoning system, can be checked by the kernel. This turns an informal open problem into a precise, machine-readable target and makes the previously proved special cases and experimental data part of a single verified corpus.","feed_headline":"The primes-are-supernatural conjecture is now a Lean proposition","feed_subtitle":"A complete Lean 4 formalization makes the open problem a named, unproved proposition automated systems can target.","key_machinery":"The load-bearing machinery is the pair of encodings of natural functions: a word-based definition FNatural using an inductive type of operation letters, and an inductive predicate IsNatural that closes the identity and constants under pointwise addition, multiplication, and exponentiation. The equivalence theorem FNatural_eq between the two is what lets every proof carry over from the paper's word formalism to structural induction on derivations. The conjecture is then a named def Conjecture_2_1 : Prop, deliberately left unproved so it contributes no axioms; all conditional results take it as an explicit hypothesis.","core_discovery":"The paper's central claim is that the statement of the primes-are-supernatural conjecture can be, and has been, formalized end to end. The class of natural functions is encoded both as a word construction and as an inductive closure; the two encodings are proved equivalent, and the conjecture -- that no non-constant natural function sends every positive integer to a prime, equivalently that the prime set is supernatural -- is stated as an exact named proposition, Conjecture_2_1, deliberately left unproved. The formalization also covers the extension of Remark 3.4 to Knuth arrows, factorial, and truncated subtraction, and it verifies all 89 experimental table rows, using kernel-checked Lucas certificates for the largest primality claims.","pith_inferences":["A machine-generated coverage check that maps each prose statement to a declaration, and a pinned commit hash, would make the completeness claim independently auditable; until then the correspondence table is only as reliable as the author's transcription.","Because the formal statement fixes the exact domain and exponent convention, an automated search for a counterexample becomes a bounded, checkable computation: any candidate function can be tested against IsNatural and Conjecture_2_1 mechanically.","The same pattern of recording a conjecture as a named Prop with explicit dependencies could be applied to other open problems in inductive-closure form, giving automated systems a standardized target.","The Lucas-certificate approach suggests that future table-heavy formalizations can move certificate data outside the kernel while keeping verification inside, trading hand-rolled primality proofs for short checked arguments."],"forward_implications":["The conjecture is now a named Lean proposition, so any claimed proof or disproof can be checked by the kernel rather than by human review.","All proved cases from the source paper -- polynomial functions, linear functions, Fermat's function, and the 89 experimental table rows -- are part of the same verified corpus.","The kernel-checked Lucas certificates show how large primality claims can be formalized without an hour-long trial division.","If the conjecture holds, the formalized Corollary 3.2 gives infinitely many composite Fermat numbers as a conditional consequence.","The extension to Knuth arrows, factorial, and truncated subtraction provides a larger class for which the analogous conjecture can be stated, with a proof that it contains the original class."],"supporting_citations":[{"why":"supplies the theorem prover and kernel that checks every declaration.","marker":"[1]"},{"why":"supplies the mathematical library, including the norm_num tactic and primality certificates used in the table proofs.","marker":"[2]"},{"why":"is the source paper whose definitions, results, and tables are being formalized; all numbered statements trace to it.","marker":"[3]"}],"fun_headline_variants":["Primes-supernatural conjecture now a precise Lean target","Lean 4 formalizes the unproved primes-supernatural conjecture","Kernel-checked: Lean 4 states the supernatural primes conjecture","Machine-checked primes-supernatural conjecture now a Lean target","Lean 4 verifies the supernatural primes conjecture statement"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the companion source file described in the paper actually compiles with the stated toolchain and that the printed declarations correspond one-to-one to that checked file; nothing in the paper itself provides a machine-checked certificate of that correspondence.","fun_headline_variants_meta":{"raw":{"variants":["Primes-supernatural conjecture now a precise Lean target","Lean 4 formalizes the unproved primes-supernatural conjecture","Kernel-checked: Lean 4 states the supernatural primes conjecture","Machine-checked primes-supernatural conjecture now a Lean target","Lean 4 verifies the supernatural primes conjecture statement"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001787,"raw_usage":{"total_tokens":6977,"prompt_tokens":810,"completion_tokens":6167,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":426,"completion_tokens_details":{"reasoning_tokens":6081}},"tokens_in":426,"tokens_out":6167,"duration_ms":46564,"temperature":1.0,"reasoning_tokens":6081,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T04:29:45.293099+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Compile the companion source file with the stated theorem prover and library versions, then inspect the named Conjecture_2_1, the correspondence-table theorems, and the #print axioms output; if any listed theorem is missing, contains sorryAx, or uses an undeclared axiom, the completeness and no-sorry claims are false.","supporting_citations":[{"cited_title":"de Moura and S","cited_arxiv_id":null,"evidence_quote":"supplies the theorem prover and kernel that checks every declaration."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"supplies the mathematical library, including the norm_num tactic and primality certificates used in the table proofs."},{"cited_title":"Mayeux,Conjecture: the set of prime numbers is supernatural, Proceed- ings of the Bulgarian Academy of Sciences78(2025), no","cited_arxiv_id":null,"evidence_quote":"is the source paper whose definitions, results, and tables are being formalized; all numbered statements trace to it."}],"review_version":1}