{"id":"84c6297f-e010-42a8-af15-0db627a0dfa0","arxiv_id":"2505.09095","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"LeanLJ computes Lennard-Jones energies and long-range corrections in periodic boundaries using Lean 4, with proofs about the mathematical functions and numerical agreement with NIST SRSW benchmarks.","lead":"The authors built LeanLJ, a Lean 4 program that computes Lennard-Jones interaction energies with periodic boundaries and matches NIST benchmark values. It is a proof-of-concept for attaching formal proofs to molecular simulation code, although the executed floating-point code is not yet fully covered by those proofs.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The executed total-energy code is not connected to the proved theorems: the displayed functions call Float-specific routines, and the paper itself concedes this gap.","rationale":"The reader identified the RealLike bridge as the weakest assumption. My reading supports that concern but locates an even more direct gap: the top-level executable functions displayed in §5.1 are Float-typed and call Float-specific functions, so even a perfectly sound RealLike instance would not make the proved Real-level theorems apply to the executed code. The paper itself acknowledges this in §7, stating that the Float version may be called instead of the polymorphic version and that Lean will not flag it. Additionally, the proved theorems in §4 are stated for lj_Real, pbc_Real, minImageDistance_Real, and U_LRC_Real; no theorem is shown that transfers these properties to lj_p, pbc, or any Float implementation. The machine-checked lemmas are real contributions, and the NIST agreement is meaningful empirical validation, but the abstract's claim that the approach 'eliminates software errors' and provides 'proofs of correctness' for the executed energy calculations is not supported by the evidence presented. This does not change the reader's conditional recommendation: the paper can be accepted if the claims are scoped to the Real-valued functions and the proof-execution connection is either machine-checked or explicitly removed from the guarantees.","tokens_in":24834,"tokens_out":6535,"duration_ms":69287,"concrete_test":"In the LeanLJ repository, locate the function actually invoked by main or totalEnergy. If it is total_energy_pairs or another Float-typed function calling minImageDistance_Float and lj_Float, the proof-execution link is absent and the concern lands. To settle it definitively, add a Lean theorem of the form: for all positions, boxLength, cutoff, epsilon, and sigma, the executed total-energy function equals the pair sum of lj(minImageDistance(...)) from Eq. 7. If Lean cannot compile such a theorem for the definitions actually executed, then the formal proofs do not certify the energy calculation.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that LeanLJ's executed energy calculation is certified by machine-checked proofs. The paper's own code and admissions break this link in two places. First, the only total-energy functions shown in §5.1 (total_energy_loop, total_energy_recursive, total_energy_pairs) are defined over Float and call minImageDistance_Float and lj_Float directly; no theorem in §4 or §5 states, let alone proves, that any of these functions equals the mathematical Upair of Eq. 7. The only summation-related theorem, pairs_length_eq, proves the number of pairs, not the energy value. Second, the RealLike bridge of §5.2 is a handwritten semantic link: RealLike declares operations but no laws, and Lean does not check that the Float instance matches the Real instance. The paper says exactly this ('mistakes in RealLike won't be flagged by Lean'). Moreover, §7 concedes that the floating-point version of a function may be called in execution instead of the polymorphic version, and Lean will not flag it. So even if every displayed Real-level lemma is correct, the executed program can differ from the proved one in ways Lean cannot detect. The NIST match is strong empirical evidence, but it is not the formal guarantee the abstract claims.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The manuscript presents LeanLJ, a Lean 4 implementation of Lennard-Jones pair-energy calculations under periodic boundary conditions. The authors formalize the LJ potential, periodic-wrap and minimum-image-distance functions, the long-range-correction integral, and a pair-list helper; they prove several lemmas about these Real-valued definitions. To make code executable, they introduce a RealLike typeclass that links Real and Float operations, and they compare Float execution against NIST SRSW benchmarks for four system sizes. The paper's stated contribution is that this approach eliminates software errors through formal logic and provides stronger guarantees than empirical benchmarking.","tokens_in":25035,"tokens_out":8381,"duration_ms":80780,"significance":"The formalization is a useful demonstration of theorem-proving technology for molecular-simulation mathematics, and the NIST comparison is a sensible empirical check. The paper is honest about several remaining trust boundaries, which is a strength. However, the advertised central claim that the executed energy calculations are formally verified is not supported by the material presented: the proved theorems concern Real-valued functions, and the paper itself identifies three unverified links (the RealLike semantics, the possible use of Float-specific definitions at runtime, and the absence of a theorem connecting total-energy execution to Eq. 7). The contribution would be publishable after a substantial revision that either closes or explicitly rescopes these gaps.","major_comments":[{"comment":"The three displayed total-energy functions (total_energy_loop, total_energy_recursive, total_energy_pairs) are all defined over Float and call minImageDistance_Float and lj_Float directly. No theorem in Section 4 or 5 states that any of these functions equals the mathematical total energy Upair of Eq. 7. The only summation-related theorem, pairs_length_eq, proves the length of the pair list, not that the list contains exactly the unordered pairs i<j or that the folded energy equals Eq. 7. Thus the executed energy value is not certified by the proofs shown. Please add a theorem connecting the executed total-energy function to Eq. 7 and a theorem that pairs enumerates each unordered pair exactly once.","section":"§5.1"},{"comment":"RealLike is declared as a typeclass listing operations and instances, but it carries no laws, and the text explicitly notes that mistakes in RealLike will not be flagged by Lean. Consequently, a theorem proved for the Real instance does not give a machine-checked guarantee about the Float instance; the semantic equivalence is a human assumption. This is a load-bearing gap for the abstract's claim of proofs of correctness for execution. The revision should either provide a formally checked connection between proof-level and execution-level semantics, or restrict the formal-verification claim to Real-valued mathematics and describe the Float code as empirically validated.","section":"§5.2"},{"comment":"The paper concedes that a floating-point version of a function may be called during execution instead of the polymorphic version and that Lean will not flag the discrepancy. This means that even the intended RealLike bridge is not enforced by the toolchain, and the proved function need not be the executed one. The execution architecture should be changed so that the executed code is definitionally the proved code, or the claim of machine-checked correctness of the executed program must be withdrawn.","section":"§7"},{"comment":"The sentence asserting that 'our confidence in our system does not stem from its agreement with the NIST benchmark, rather from the theorems we have proved' is not supported for the total-energy value, because the theorems do not cover the total-energy Float function. The paper should state precisely which components are theorem-backed (the Real-valued definitions and lemmas) and which are only benchmark-backed (the Float total energy), rather than attributing the NIST agreement to the proofs.","section":"§7 (Discussion)"}],"minor_comments":[{"comment":"The theorem cutoff_behaviour applies lj_Real with arguments ε σ r r_c, but lj_Real is defined with argument order r r_c ε σ; please correct the order or the definition.","section":"§4.2"},{"comment":"In long_range_correction_equality, the right-hand side 'U_LRC ρ ε σ rc π' appears to apply five arguments to a four-argument function; the final π is likely a transcription error and should be removed.","section":"§4.5"},{"comment":"The theorem statement of squaredminImageDistance_theorem uses box_length in the last argument of the RHS while the definition and the LHS use boxLength; unify the spelling.","section":"§4.4"},{"comment":"The fraction in Eq. (8) is rendered as '1 24πρ', which is ambiguous; please use standard notation and check the prefactor against the formula in Eq. (11).","section":"Eq. (8)"},{"comment":"The phrase 'machine precision' is stronger than what Table 2 demonstrates, which is agreement to the number of digits reported by NIST; please rephrase to 'agreement to the reported digits.'","section":"§7"},{"comment":"The theorem pairs_length_eq is stated but its proof is omitted from the paper and deferred to GitHub; please state the full theorem statement in the text and indicate the auxiliary lemmas it relies on.","section":"§5.1"}],"recommendation":"major_revision","confidential_remarks":"This is more of a formal-methods and software-engineering demonstration than a new statistical-mechanics result, which may affect fit with the journal's scope. The main concern is the gap between the advertised guarantee and the implemented artifact; I would support acceptance only after the claims are rescoped or the gaps are closed. No citation or novelty concerns otherwise."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Punchline: this is a real proof-of-concept for using Lean in molecular simulation, but the executed Float code is not the object of the proved theorems, and the paper says so itself. The abstract's \"eliminates software errors... proofs of correctness\" overstates what is demonstrated.\n\nWhat's new: LeanLJ is, as far as I know, the first Lean implementation that both proves properties of a Lennard-Jones energy calculation and runs it against external benchmarks. The earlier group paper only formalized derivations; Certigrad is about ML, not molecular simulation. The Real-level results are standard but machine-checked: lj_eq, cutoff behavior, abs_pbc_le, minImageDistance_self, long-range correction equality, pairs_length_eq. The NIST SRSW match on four systems is real, with no fitted parameters, and code and proofs are on GitHub. The authors are also unusually candid about remaining failure modes, including the RealLike bridge and IO.\n\nThe soft spot is central. The proved theorems are about noncomputable Real-valued functions. The functions that actually run—total_energy_loop, total_energy_recursive, total_energy_pairs in §5.1—are Float-specific and call minImageDistance_Float and lj_Float directly; no theorem states that any of these equals the mathematical Upair of Eq. 7. RealLike is a handwritten typeclass with no laws; Lean does not check that the Float instance matches the Real operations. The paper admits exactly this, and Section 7 adds that the floating-point version could be called in execution instead of the polymorphic one without Lean flagging it. So the NIST agreement is empirical evidence, not the formal guarantee the abstract claims. The individual theorems are fine; the link between theorem and executable is not machine-checked.\n\nThat gap is load-bearing only if you read the paper at its strongest. If the paper were reframed as \"formally verified Real-valued components plus an empirically validated Float implementation,\" the objection mostly disappears. For a proof-of-concept, the four test systems and LJ-only scope are acceptable.\n\nWho this is for: people working on formal verification of scientific software, and simulation developers who want a glimpse of where the field could go. I would bring it to a reading group.\n\nMy call: send it to peer review, but require a major revision that scopes the claims and states explicitly which components are proved and which are tested.","headline":"A genuine Lean proof-of-concept for molecular energy calculations, but the abstract overclaims: the executed Float code is not connected to the proved Real-valued theorems, and the paper itself admits the gap.","tokens_in":25557,"tokens_out":2965,"would_cite":true,"duration_ms":32513,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68V20","68Q60","03B35"],"pacs":[],"model":"deepseek-v4-flash","headline":"Formal proofs, not just tests, certify a Lennard-Jones energy calculator.","keywords":["formal verification","Lean 4","molecular simulation","Lennard-Jones potential","periodic boundary conditions","minimum image convention","typeclasses","long-range correction"],"falsifier":"A cheap decisive check is to call the polymorphic round function on 0.5 and compare it with the floating-point primitive; if the RealLike instance maps round to a Real rounding that differs from Float's half-to-even rule, the periodic-boundary certificate for the executed code is void even though every Lean proof checks out.","tokens_in":24612,"feed_emoji":"✅","tokens_out":6261,"duration_ms":60250,"temperature":0.7,"pith_summary":"This paper sets out to show that formal proof can serve as the primary correctness guarantee for a concrete scientific computing task, replacing reliance on testing and human inspection. It presents LeanLJ, a Lennard-Jones energy calculator written in the Lean proof assistant, whose mathematical components—the pair potential, periodic wrapping, minimum-image distance, and long-range correction—are accompanied by machine-checked theorems. The same polymorphic code is instantiated over real numbers for proofs and over floating-point numbers for execution, and the executed program reproduces the gold-standard reference benchmark values for four systems to the printed precision. The authors claim the proofs, not the benchmark match, are what make the software trustworthy. If the approach is right, it opens a route toward molecular simulation code that is correct by construction.","feed_headline":"Machine-checked proofs certify Lennard-Jones energy code","feed_subtitle":"The same code proven against ideal reals runs on floats, matching reference energies to the printed digits.","key_machinery":"The load-bearing mechanism is the RealLike typeclass, a hand-written bundle that equips any numeric type with the arithmetic, comparison, rounding, and square-root operations used in the energy calculation, together with separate instances for the real numbers and for floating-point numbers. Every executable function—periodic wrapping, minimum-image distance, Lennard-Jones potential, pair summation, long-range correction—is written polymorphically over this typeclass, so Lean can reason about the real-number instance in proofs and run the floating-point instance in practice. The proofs that carry the argument are the ones linking representations and properties: lj_eq equates the efficient r3/r6/r12 form with the textbook potential, abs_pbc_le bounds wrapped coordinates, minImageDistance_real_self and minImageDistance_real_nonneg constrain distances, pairs_length_eq fixes the pair count at N(N-1)/2, and long_range_correction_equality connects the correction formula to its integral definition.","core_discovery":"The central claim is that LeanLJ reproduces the benchmark Lennard-Jones pair energies and long-range corrections for particle counts 30, 200, 400, and 800, while providing machine-checked proofs about the mathematics those numbers come from. The theorems certify, for example, that the wrapped position always lies within [-L/2, L/2], that the minimum-image distance between a particle and itself is zero and is always non-negative, that the implemented Lennard-Jones form equals the textbook form, and that the long-range correction is the integral of the truncated potential over (rc, infinity). Because the executable code is the polymorphic version of those same functions, the authors assert that the guarantees transfer from the real-valued idealization to the floating-point execution, making LeanLJ a stronger benchmark than empirical reference values alone.","pith_inferences":["The RealLike caveat suggests a concrete strengthening: if the rounding and square-root semantics were generated from a single formal specification rather than written twice by hand, Lean could check the link and the human oversight step would disappear.","Because the proofs are over real numbers, floating-point round-off remains outside the certificate; combining this approach with interval arithmetic would extend the guarantee from 'correct math, executed' to 'correct math, executed within a certified error bound.'","A library of formally verified reference energies for standard test systems could shift benchmarking practice: a new simulator could be checked against a proof-backed oracle, making disagreement a theorem rather than a judgement call.","The same polymorphic bridge could apply to any scientific code with a clean real-valued idealization, such as integrators, solvers, or statistical-mechanics estimators, not just energy calculations."],"forward_implications":["Anyone running LeanLJ's floating-point code gets benchmark-matching energies for the four tested systems, plus the guarantee that the same algorithm satisfies the proved mathematical properties.","The pair-counting theorem eliminates an entire class of off-by-one summation bugs without needing test data, since Lean checks both termination and the N(N-1)/2 pair count.","The same polymorphism strategy can be carried over to other pair potentials, cutoff treatments, and eventually Coulomb sums and neighbour lists, as the outlook states.","Formally verified energy calculations could serve as a reference oracle: workflows that generate inputs for both verified software and conventional simulators could flag deviations as bugs in the conventional package.","The continuity theorem on the closed domain identifies exactly where the truncated Lennard-Jones function is and is not smooth, which matters for force evaluation in molecular dynamics."],"supporting_citations":[{"why":"Supplies the reference benchmark energies for the four Lennard-Jones systems against which LeanLJ results are compared.","marker":"[37]"},{"why":"Provides the periodic boundary condition, minimum image convention, and Lennard-Jones formulations that the formal definitions encode.","marker":"[7]"},{"why":"Source of the long-range correction integral that U_LRC_Real is proved to satisfy.","marker":"[25]"},{"why":"Models the hybrid proof-plus-test strategy and the idea of linking verified mathematics to executable code.","marker":"[41]"},{"why":"Introduces the Lean 4 theorem prover and programming language in which LeanLJ is written.","marker":"[45]"},{"why":"Supplies the functional-programming background: recursion, tail recursion, monads, and termination checking used in the executable layer.","marker":"[46]"},{"why":"The authors' earlier formalization of chemical physics, which this work extends from proofs alone to executable programs.","marker":"[47]"}],"fun_headline_variants":["Lean-verified LJ code matches NIST benchmarks","Formal proofs guarantee energy code matches NIST","Machine-checked energy calculations, proven in Lean","Lean theorem prover verifies energy benchmarks","LeanLJ: formally verified Lennard-Jones energy code"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is the hand-written correspondence between the idealized real-number operations that the proofs reason about and the floating-point operations that actually run; Lean checks the proofs but does not check this correspondence, so a wrong link would silently void the guarantee.","fun_headline_variants_meta":{"raw":{"variants":["Lean-verified LJ code matches NIST benchmarks","Formal proofs guarantee energy code matches NIST","Machine-checked energy calculations, proven in Lean","Lean theorem prover verifies energy benchmarks","LeanLJ: formally verified Lennard-Jones energy code"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001783,"raw_usage":{"total_tokens":6990,"prompt_tokens":868,"completion_tokens":6122,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":484,"completion_tokens_details":{"reasoning_tokens":6050}},"tokens_in":484,"tokens_out":6122,"duration_ms":46747,"temperature":1.0,"reasoning_tokens":6050,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T21:40:07.289406+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A cheap decisive check is to call the polymorphic round function on 0.5 and compare it with the floating-point primitive; if the RealLike instance maps round to a Real rounding that differs from Float's half-to-even rule, the periodic-boundary certificate for the executed code is void even though every Lean proof checks out.","supporting_citations":[{"cited_title":"Tildesley","cited_arxiv_id":null,"evidence_quote":"Provides the periodic boundary condition, minimum image convention, and Lennard-Jones formulations that the formal definitions encode."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Source of the long-range correction integral that U_LRC_Real is proved to satisfy."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Models the hybrid proof-plus-test strategy and the idea of linking verified mathematics to executable code."},{"cited_title":"The Lean 4 Theorem Prover and Programming Lan- guage","cited_arxiv_id":null,"evidence_quote":"Introduces the Lean 4 theorem prover and programming language in which LeanLJ is written."},{"cited_title":"Functional Programming in Lean","cited_arxiv_id":null,"evidence_quote":"Supplies the functional-programming background: recursion, tail recursion, monads, and termination checking used in the executable layer."},{"cited_title":"Bobbin, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang, Catherine M","cited_arxiv_id":null,"evidence_quote":"The authors' earlier formalization of chemical physics, which this work extends from proofs alone to executable programs."}],"review_version":1}