Pith. sign in

REVIEW 4 major objections 6 minor 61 references

Benchmarking Energy Calculations Using Formal Proofs

T0 review · 4 major / 6 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Formal proofs, not just tests, certify a Lennard-Jones energy calculator.

desk verdict 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. read the letter →

arxiv 2505.09095 v2 pith:SY5JV6O7 submitted 2025-05-14 cond-mat.stat-mech

Ejike D. Ugwuanyi , Colin T. Jones , John Velkey , Tyler R. Josephson This is my paper · ORCID
classification cond-mat.stat-mech MSC 68V2068Q6003B35
keywords formalverificationLean4molecularsimulationLennard-Jonespotentialperiodicboundaryconditionsminimumimageconventiontypeclasseslong-rangecorrection
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 6 minor

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.

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 (4)
  1. [§5.1] 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.
  2. [§5.2] 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.
  3. [§7] 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.
  4. [§7 (Discussion)] 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.
minor comments (6)
  1. [§4.2] 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.
  2. [§4.5] 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.
  3. [§4.4] 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.
  4. [Eq. (8)] 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).
  5. [§7] 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.'
  6. [§5.1] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the energy values are externally benchmarked and the proofs are machine-checked; the admitted RealLike gap is a correctness caveat, not circularity.

full rationale

The derivation chain is self-contained and externally anchored. The Lennard-Jones pair energy, minimum-image distance, periodic wrapping, and long-range correction follow standard mathematical definitions (Eqs. 1-11), and the Lean theorems (lj_eq, cutoff_behaviour, abs_pbc_le, long_range_correction_equality) are machine-checked proofs about Real-valued functions, not fitted quantities. The NIST SRSW comparison in Section 6 is an external benchmark, and no parameter is fitted to it. The only reliance on the authors' prior work is contextual ([47]), and it is not load-bearing. The paper explicitly acknowledges the limits of the RealLike bridge in Sections 5.2 and 7: 'mistakes in RealLike won't be flagged by Lean' and 'proofs for that function are not technically connected to the execution'; these admissions narrow the strength of the certified-execution claim, but they are not a circular reduction of the result to its inputs. No equation is defined in terms of its own prediction, no fitted input is renamed as a prediction, and no uniqueness theorem is imported from self-citation. Thus the correct circularity finding is none.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

No free parameters are fitted: epsilon, sigma, cutoff, density, and box length are inputs from the benchmark or standard model. The physics enters through the Lennard-Jones potential, periodic boundaries, cutoff truncation, and long-range correction formulas. The most fragile assumption is the manual RealLike bridge between Real proofs and Float execution, which the authors explicitly identify as unverified. No new physical entities are introduced.

assumptions (6)
  • standard math The Lean kernel and Mathlib are sound.
    Section 7 (first source of uncertainty): 'we are trusting in the axioms of mathematics, as expressed in Lean's core; errors here might compromise Mathlib, on which we depend.'
  • ad hoc to paper RealLike correctly maps Real operations used in proofs to Float operations used in execution.
    Section 5.2 defines RealLike manually; the authors state 'mistakes in RealLike won't be flagged by Lean' and 'the human is responsible for ensuring correct semantics.'
  • domain assumption The Lennard-Jones potential with cutoff truncation is the model to compute.
    Section 3, Eqs 1 and 6; standard force field not derived in this paper.
  • domain assumption Periodic boundary conditions and the minimum image convention model the bulk fluid.
    Section 3, Eqs 2-5, following Allen and Tildesley.
  • domain assumption The long-range correction assumes pair correlation g(r)=1 beyond the cutoff.
    Eqs 8-11; this is the standard tail-correction approximation.
  • domain assumption NIST SRSW benchmark values are correct reference values.
    Section 6 compares LeanLJ output to NIST; this external reference is taken as ground truth.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Benchmarking Energy Calculations Using Formal Proofs." pith.science (2026). https://pith.science/paper/SY5JV6O7

@misc{pith2026250509095,
  author       = {Pith},
  title        = {Pith review of: Benchmarking Energy Calculations Using Formal Proofs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SY5JV6O7}},
  note         = {Machine review of arXiv:2505.09095}
}
read the original abstract

Traditional approaches for validating molecular simulations rely on making software open source and transparent, incorporating unit testing, and generally employing human oversight. We propose an approach that eliminates software errors using formal logic, providing proofs of correctness. We use the Lean theorem prover and programming language to create a rigorous, mathematically verified framework for computing molecular interaction energies. We demonstrate this in LeanLJ, a package of functions, proofs, and code execution software that implements Lennard Jones energy calculations in periodic boundaries. We introduce a strategy that uses polymorphic functions and typeclasses to bridge formal proofs (about idealized Real numbers) and executable programs (over floating point numbers). Execution of LeanLJ matches the current gold standard NIST benchmarks, while providing even stronger guarantees, given LeanLJ's grounding in formal mathematics. This approach can be extended to formally verified molecular simulations, in particular, and formally verified scientific computing software, in general. Keywords: Formal verification, Lean 4, molecular simulations, functional programming.

Figures

Figures reproduced from arXiv: 2505.09095 by the authors.

Figure 1
Figure 1. Comparison of code correctness approaches (adapted from [ [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. (a) Periodic boundary conditions: Particles outside the central cubic simulation box are wrapped [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. The Lennard-Jones potential, truncated at the cut-off. [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Workflow of the Lennard-Jones energy calculation using LeanLJ. The process involves recursive [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]
Figure 5
Figure 5. Figure 5: How polymorphic functions link proofs (over idealized Real numbers) with execution (over float [PITH_FULL_IMAGE:figures/full_fig_p016_5.png]
Figure 6
Figure 6. Figure 6: Explanation of the polymorphic pbc function. The function is defined over a generic type α, and the required operations—subtraction, multiplication, division, and rounding—are expressed through type classes: HSub, HMul, HDiv, and HasRound. Each type class specifies tha…
Figure 7
Figure 7. Figure 7: The IO Monad as a bridge that links the verified, pure functions in Lean with the messy real world, [PITH_FULL_IMAGE:figures/full_fig_p020_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

61 extracted references · 47 canonical work pages

  1. [1]

    Hugo A. L. Filipe and Luís M. S. Loura. Molecular Dynamics Simulations: Advances and Applica- tions. Molecules, 27(7):2105, March 2022. URL: https://www.mdpi.com/1420-3049/27/7/2105, doi:10.3390/molecules27072105

    work page doi:10.3390/molecules27072105 2022

  2. [2]

    Accurate van der Waals force field for gas adsorption in porous materials

    Lei Sun, Li Yang, Ya-Dong Zhang, Qi Shi, Rui-Feng Lu, and Wei-Qiao Deng. Accurate van der Waals force field for gas adsorption in porous materials. Journal of Computational Chemistry, 38(23):1991– 1999, September 2017. URL: https://onlinelibrary.wiley.com/doi/10.1002/jcc.24832, doi:10.1002/jcc.24832

    work page doi:10.1002/jcc.24832 1991

  3. [3]

    Progress and Prospect of Theoretical Simulation of Microporous Materials

    Lei Sun and Weiqiao Deng. Progress and Prospect of Theoretical Simulation of Microporous Materials. Acta Chimica Sinica, 73(6):579, 2015. URL: http://sioc-journal.cn/Jwk_hxxb/CN/abstract/ abstract344992.shtml, doi:10.6023/A15030192

    work page doi:10.6023/a15030192 2015

  4. [4]

    Mark and Wilfred F

    Alan E. Mark and Wilfred F. Van Gunsteren. Decomposition of the Free Energy of a Sys- tem in Terms of Specific Interactions. Journal of Molecular Biology , 240(2):167–176, July

    work page

  5. [5]

    Raphael S. Alvim. Material Surfaces and Interfaces: Characterization, Molecular Adsorption and Heterogeneous Catalysis by Computational Simulation. Revista Virtual de Química , 15(2):262– 282, 2023. URL: https://rvq.sbq.org.br/audiencia_pdf.asp?aid2=1571&nomeArquivo= v15n2a07.pdf, doi:10.21577/1984-6835.20220124. 24

    work page arXiv 2023

  6. [6]

    Molecular Modelling: Principles and Applications

    Andrew R Leach. Molecular Modelling: Principles and Applications . Prentice Hall, 2nd edition, 2001

    work page 2001

  7. [7]

    Tildesley

    Michael Patrick Allen and Dominic J. Tildesley. Computer simulation of liquids . Oxford University Press, Oxford, 2nd ed edition, 2017

    work page 2017

  8. [8]

    Experiments

    Loup Verlet. Computer "Experiments" on Classical Fluids. I. Thermodynamical Properties of Lennard- Jones Molecules. Physical Review, 159(1):98–103, July 1967. URL: https://link.aps.org/doi/ 10.1103/PhysRev.159.98, doi:10.1103/PhysRev.159.98

    doi:10.1103/physrev.159.98 1967

Show all 61 references
  1. [9]

    Horton, Simon Boothroyd, Pavan Kumar Behara, David L

    Joshua T. Horton, Simon Boothroyd, Pavan Kumar Behara, David L. Mobley, and Daniel J. Cole. A transferable double exponential potential for condensed phase simulations of small molecules. Digital Discovery, 2(4):1178–1187, 2023. URL: https://xlink.rsc.org/?DOI=D3DD00070B, doi:...

    2023

  2. [10]

    A Brief Review on Results and Computational Algorithms for Minimizing the Lennard- Jones Potential, December 2010

    Jiapu Zhang. A Brief Review on Results and Computational Algorithms for Minimizing the Lennard- Jones Potential, December 2010. arXiv:1101.0039 [physics]. URL: http://arxiv.org/abs/1101. 0039, doi:10.48550/arXiv.1101.0039

    2010 doi arXiv

  3. [11]

    Integrated Lennard-Jones Potential between a Sphere and a Thin Rod, May 2024

    Junwen Wang and Shengfeng Cheng. Integrated Lennard-Jones Potential between a Sphere and a Thin Rod, May 2024. arXiv:2405.03944 [cond-mat]. URL: http://arxiv.org/abs/2405.03944, doi:10.48550/arXiv.2405.03944

    2024 doi arXiv

  4. [12]

    Peter Schwerdtfeger, Antony Burrows, and Odile R. Smits. The Lennard Jones Potential Revisited – Analytical Expressions for Vibrational Effects in Cubic and Hexagonal Close-Packed Lattices. The Journal of Physical Chemistry A , 125(14):3037–3057, April 2021. arXiv:2012.05413 [...

    2021 arXiv

  5. [13]

    The Lennard-Jones potential: when (not) to use it

    Xipeng Wang, Simón Ramírez-Hinestrosa, Jure Dobnikar, and Daan Frenkel. The Lennard-Jones potential: when (not) to use it. Physical Chemistry Chemical Physics , 22(19):10624–10633, May

  6. [14]

    A. Rahman. Correlations in the Motion of Atoms in Liquid Argon. Physical Review, 136(2A):A405– A411, October 1964. URL: https://link.aps.org/doi/10.1103/PhysRev.136.A405, doi:10. 1103/PhysRev.136.A405

    1964 doi

  7. [15]

    A new correlation model for predicting the melting and boiling temperatures of the Lennard-Jones systems

    Chenyang Sun, Yaning Zhang, Chaofeng Hou, and Wei Ge. A new correlation model for predicting the melting and boiling temperatures of the Lennard-Jones systems. Physica Scripta, 98(1):015702, Jan- uary 2023. URL: https://iopscience.iop.org/article/10.1088/1402-4896/aca443, doi:...

    2023 doi

  8. [16]

    Nicolas, K.E

    J.J. Nicolas, K.E. Gubbins, W.B. Streett, and D.J. Tildesley. Equation of state for the Lennard-Jones fluid. Molecular Physics, 37(5):1429–1454, May 1979. URL: https://www.tandfonline.com/ doi/full/10.1080/00268977900101051, doi:10.1080/00268977900101051

    1979 doi

  9. [17]

    Ronald Fawcett

    W. Ronald Fawcett. Electrolyte Solutions. In Liquids, Solutions, and Interfaces . Oxford University Press, July 2004. URL: https://academic.oup.com/book/40724/chapter/348485529, doi: 10.1093/oso/9780195094329.003.0007

    2004

  10. [18]

    Charged colloids, polyelectrolytes and biomolecules viewed as strongly coupled Coulomb systems

    H L Wen, E Allahyarov, C N Likos, R Blaak, J Dzubiella, A Jusufi, N Hoffmann, and H M Harreis. Charged colloids, polyelectrolytes and biomolecules viewed as strongly coupled Coulomb systems. Journal of Physics A: Mathematical and General , 36(22):5827–5834, June

  11. [19]

    Dean, Jure Dobnikar, Ali Naji, and Rudolf Podgornik, editors

    David S. Dean, Jure Dobnikar, Ali Naji, and Rudolf Podgornik, editors. Electrostatics of Soft and Disordered Matter . Jenny Stanford Publishing, 0 edition, May 2014. URL: https://www. taylorfrancis.com/books/9789814411868, doi:10.1201/b15597

    2014

  12. [20]

    Yang and Xiantao Li

    Jerry Z. Yang and Xiantao Li. Comparative study of boundary conditions for molecular dynamics simulations of solids at low temperature.Physical Review B, 73(22):224111, June 2006. URL: https: //link.aps.org/doi/10.1103/PhysRevB.73.224111, doi:10.1103/PhysRevB.73.224111. 25

    2006 doi

  13. [21]

    Dudek, Brian Ellul, and Joseph N

    Luke Mizzi, Daphne Attard, Ruben Gatt, Krzysztof K. Dudek, Brian Ellul, and Joseph N. Grima. Implementation of periodic boundary conditions for loading of mechanical metamate- rials and other complex geometric microstructures using finite element analysis. Engineering with Com...

    2021 doi

  14. [22]

    Bull-Vulpe, Xuanyu Zhu, Henry Agnew, Shreya Gupta, Suman Saha, and Francesco Paesani

    Etienne Palos, Ethan F. Bull-Vulpe, Xuanyu Zhu, Henry Agnew, Shreya Gupta, Suman Saha, and Francesco Paesani. Current Status of the MB-pol Data-Driven Many-Body Po- tential for Predictive Simulations of Water Across Different Phases, September 2024. URL: https://chemrxiv.org/e...

    2024 doi

  15. [23]

    Atomistic Simulations of Ionic Liquid and Polymer Elec- trolytes: From Bulk Phases to Interfacial Behavior

    John W Lawson and Justin B Haskins. Atomistic Simulations of Ionic Liquid and Polymer Elec- trolytes: From Bulk Phases to Interfacial Behavior. ECS Meeting Abstracts, MA2017-01(22):1147– 1147, April 2017. URL: https://iopscience.iop.org/article/10.1149/MA2017-01/22/ 1147, doi:...

    2017 doi

  16. [24]

    Andrews and Estela Blaisten-Barojas

    James P. Andrews and Estela Blaisten-Barojas. Workflow for investigating thermodynamic, struc- tural and energy properties of condensed polymer systems from Molecular Dynamics, 2022. Version Number: 1. URL: https://arxiv.org/abs/2203.02819, doi:10.48550/ARXIV.2203.02819

    2022 doi arXiv

  17. [25]

    W. W. Wood and F. R. Parker. Monte Carlo Equation of State of Molecules Interacting with the Lennard-Jones Potential. I. A Supercritical Isotherm at about Twice the Critical Temperature. The Journal of Chemical Physics , 27(3):720–733, September 1957. URL: https://pubs.aip.org...

    1957

  18. [26]

    Fast Parallel Algorithms for Short-Range Molecular Dynamics

    Steve Plimpton. Fast Parallel Algorithms for Short-Range Molecular Dynamics. Journal of Computa- tional Physics, 117(1):1–19, March 1995. URL: https://linkinghub.elsevier.com/retrieve/ pii/S002199918571039X, doi:10.1006/jcph.1995.1039

    1995

  19. [27]

    Smith, Berk Hess, and Erik Lindahl

    Mark James Abraham, Teemu Murtola, Roland Schulz, Szilárd Páll, Jeremy C. Smith, Berk Hess, and Erik Lindahl. GROMACS: High performance molecular simulations through multi-level parallelism from laptops to supercomputers. SoftwareX, 1-2:19–25, September

  20. [28]

    Mark, and Herman J

    David Van Der Spoel, Erik Lindahl, Berk Hess, Gerrit Groenhof, Alan E. Mark, and Herman J. C. Berendsen. GROMACS: Fast, flexible, and free. Journal of Computational Chemistry, 26(16):1701– 1718, December 2005. URL: https://onlinelibrary.wiley.com/doi/10.1002/jcc.20291, doi:10....

    2005 doi

  21. [30]

    Mobley, J

    Anthony Nicholls, David L. Mobley, J. Peter Guthrie, John D. Chodera, Christopher I. Bayly, Matthew D. Cooper, and Vijay S. Pande. Predicting Small-Molecule Solvation Free Energies: An Informal Blind Test for Computational Chemistry. Journal of Medicinal Chemistry , 51(4):769–...

    2008 doi

  22. [31]

    Friend, David J

    Daniel G. Friend, David J. Frurip, Joseph W. Magee, and James D. Olson. Establishing bench- marks for the first industrial fluids simulation challenge. Fluid Phase Equilibria , 217(1):11–15, March 2004. URL: https://linkinghub.elsevier.com/retrieve/pii/S0378381203003571, doi:1...

    2004 doi

  23. [32]

    The first industrial fluid properties simulation challenge

    Fiona Case, Anne Chaka, Daniel G Friend, David Frurip, Joseph Golab, Russell Johnson, Jonathan Moore, Raymond D Mountain, James Olson, Martin Schiller, and Joey Storer. The first industrial fluid properties simulation challenge. Fluid Phase Equilibria , 217(1):1–10, March

  24. [33]

    Craven, Ramanish Singh, Co D

    Nicholas C. Craven, Ramanish Singh, Co D. Quach, Justin B. Gilmer, Brad Crawford, Eliseo Marin- Rimoldi, Ryan Smith, Ryan DeFever, Maxim S. Dyukov, Jenny W. Fothergill, Chris Jones, Timothy C. Moore, Brandon L. Butler, Joshua A. Anderson, Christopher R. Iacovella, Eric Jankows...

    2025

  25. [34]

    Quach, Nicholas C

    Brad Crawford, Umesh Timalsina, Co D. Quach, Nicholas C. Craven, Justin B. Gilmer, Clare McCabe, Peter T. Cummings, and Jeffrey J. Potoff. MoSDeF-GOMC: Python Software for the Creation of Scientific Workflows for the Monte Carlo Simulation Engine GOMC.Journal of Chemical Infor...

    2023 doi

  26. [35]

    Nash, Mohammad Mostafanejad, T

    Jessica A. Nash, Mohammad Mostafanejad, T. Daniel Crawford, and Ashley Ringer McDonald. MolSSI Education: Empowering the Next Generation of Computational Molecular Scientists. Com- puting in Science & Engineering, 24(3):72–76, May 2022. URL: https://ieeexplore.ieee.org/ docume...

    2022

  27. [36]

    Thompson, Justin B

    Matthew W. Thompson, Justin B. Gilmer, Ray A. Matsumoto, Co D. Quach, Parashara Shamaprasad, Alexander H. Yang, Christopher R. Iacovella, Clare McCabe, and Peter T. Cummings. Towards molec- ular simulations that are transparent, reproducible, usable by others, and extensible (...

    2020

  28. [37]

    Shen, Daniel W

    Vincent K. Shen, Daniel W. Siderius, William P. Krekelberg, and Harold W. Hatch, editors. NIST Standard Reference Simulation Website. Number 173 in NIST Standard Reference Database. National Institute of Standards and Technology, Gaithersburg, MD, 20899, 2017. URL: https://doi...

    2017 doi

  29. [38]

    Merz and Michael R

    Pascal T. Merz and Michael R. Shirts. Testing for physical validity in molecular simulations. PLOS ONE, 13(9):e0202764, September 2018. URL: https://dx.plos.org/10.1371/journal.pone. 0202764, doi:10.1371/journal.pone.0202764

    2018 doi

  30. [39]

    D. Price. Pentium FDIV flaw-lessons learned. IEEE Micro, 15(2):86–88, April 1995. URL: https: //ieeexplore.ieee.org/document/372360/, doi:10.1109/40.372360

    1995 doi

  31. [40]

    Kaivola and N

    R. Kaivola and N. Narasimhan. Formal Verification of the Pentium® 4 Floating-Point Multiplier. In Proceedings of the conference on Design, automation and test in Europe , DATE ’02, page 20, USA, March 2002. IEEE Computer Society

    2002

  32. [41]

    Daniel Selsam, Percy Liang, and David L. Dill. Developing Bug-Free Machine Learning Systems With Formal Mathematics. InProceedings of the 34th International Conference on Machine Learning, pages 3047–3056. PMLR, July 2017. ISSN: 2640-3498. URL: https://proceedings.mlr.press/v7...

    2017

  33. [42]

    Floating-Point Verification Using Theorem Proving

    John Harrison. Floating-Point Verification Using Theorem Proving. In Marco Bernardo and Alessan- dro Cimatti, editors, Formal Methods for Hardware Verification , volume 3965, pages 211–242. Springer Berlin Heidelberg, Berlin, Heidelberg, 2006. Series Title: Lecture Notes in Co...

    2006 doi

  34. [43]

    Tran and Yan Wang

    Anh V . Tran and Yan Wang. Reliable Molecular Dynamics: Uncertainty quantification using interval analysis in molecular dynamics simulation. Computational Materials Science, 127:141–160, February

  35. [44]

    Conservative Interval Arithmetic in Lean, March 2025

    Geoffrey Irving. Conservative Interval Arithmetic in Lean, March 2025. original-date: 2024-05- 26T10:00:08Z. URL: https://github.com/girving/interval

    2025

  36. [45]

    The Lean 4 Theorem Prover and Programming Lan- guage

    Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Lan- guage. In Automated Deduction – CADE 28 , volume 12699, pages 625–635, Cham, 2021. Springer International Publishing. URL: https://lean-lang.org/papers/lean4.pdf, doi:10.1007/ 978-3-030-798...

    2021

  37. [46]

    Functional Programming in Lean

    David Thrane Christiansen. Functional Programming in Lean. Leanprover Community, 2023. URL: https://leanprover.github.io/functional_programming_in_lean/

    2023

  38. [47]

    Bobbin, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang, Catherine M

    Maxwell P. Bobbin, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang, Catherine M. Wraback, and Tyler R. Josephson. Formalizing chemical physics using the Lean theorem prover. Digital Dis- covery, 3(2):264–280, 2024. URL: https://xlink.rsc.org/?DOI=D3DD00077J, doi:10.1039/ D3DD00077J

    2024

  39. [48]

    HepLean: Digitalising high energy physics, May 2024

    Joseph Tooby-Smith. HepLean: Digitalising high energy physics, May 2024. arXiv:2405.08863 [hep- ph]. URL: http://arxiv.org/abs/2405.08863, doi:10.48550/arXiv.2405.08863

    2024 doi arXiv

  40. [49]

    lecopivo/SciLean, April 2025

    Tomáš Sk ˇrivan. lecopivo/SciLean, April 2025. original-date: 2021-09-27T21:50:10Z. URL: https: //github.com/lecopivo/SciLean

    2025

  41. [50]

    The Mechanics of Proof

    Heather Macbeth. The Mechanics of Proof . 2022. URL: https://hrmacbeth.github.io/ math2001/index.html

    2022

  42. [51]

    Understanding molecular simulation: from algorithms to applications

    Daan Frenkel and Berend Smit. Understanding molecular simulation: from algorithms to applications. Number 1 in Computational science series. Academic Press, San Diego, 2nd ed edition, 2002

    2002

  43. [52]

    The Lean Theorem Prover (System Description)

    Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Amy P. Felty and Aart Middeldorp, editors,Automated Deduction - CADE-25 , pages 378–388, Cham, 2015. Springer International Publishing. doi:1...

    2015

  44. [53]

    ComputableReal: A Lean library for computable real numbers,

    Alex Meiburg and Johan Commelin. ComputableReal: A Lean library for computable real numbers,

  45. [54]

    Summers, Justin B

    Andrew Z. Summers, Justin B. Gilmer, Christopher R. Iacovella, Peter T. Cummings, and Clare MCabe. MoSDeF, a Python Framework Enabling Large-Scale Computational Screening of Soft Mat- ter: Application to Chemistry-Property Relationships in Lubricating Monolayer Films. Journal ...

    2020 doi

  46. [55]

    Formalization of physics index notation in Lean 4, November 2024

    Joseph Tooby-Smith. Formalization of physics index notation in Lean 4, November 2024. arXiv:2411.07667 [cs]. URL: http://arxiv.org/abs/2411.07667, doi:10.48550/arXiv. 2411.07667

    2024 doi arXiv

  47. [1994]

    URL: https://linkinghub.elsevier.com/retrieve/pii/S0022283684714306, doi: 10.1006/jmbi.1994.1430

    1994

  48. [2003]

    URL: https://iopscience.iop.org/article/10.1088/0305-4470/36/22/301, doi: 10.1088/0305-4470/36/22/301

    doi

  49. [2004]

    URL: https://linkinghub.elsevier.com/retrieve/pii/S0378381203002085, doi: 10.1016/S0378-3812(03)00208-5. 26

    doi

  50. [2015]

    URL: https://linkinghub.elsevier.com/retrieve/pii/S2352711015000059, doi: 10.1016/j.softx.2015.06.001

    2015 doi

  51. [2017]

    URL: https://linkinghub.elsevier.com/retrieve/pii/S0927025616305171, doi: 10.1016/j.commatsci.2016.10.021

    2016 doi

  52. [2020]

    URL: https://pubs.rsc.org/en/content/ articlelanding/2020/cp/c9cp05445f, doi:10.1039/C9CP05445F

    Publisher: The Royal Society of Chemistry. URL: https://pubs.rsc.org/en/content/ articlelanding/2020/cp/c9cp05445f, doi:10.1039/C9CP05445F

    2020 doi

  53. [2025]

    URL: https://github.com/Timeroot/ComputableReal

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.