Bibliography

The codes the map cites

Each code on this page has a representation on the map: a record of which quantities the code computes, through which interface, with a citation, a DOI where one exists, and the code's license.

The bibliography

Entries are sorted by the number of quantities they serve, then by name.

Loading the bibliography…

Lean, the prover behind the formula proofs

Lean 4 is a proof assistant. One Lean package, pinned to one Physlib revision, declares the map's node dimensions and proves conditional theorems about its formulas, and the build has no sorry placeholders. The Lean page lists the coverage and the limits of the proofs.

Cited works:

  • L. de Moura and S. Ullrich, "The Lean 4 theorem prover and programming language", CADE-28 (2021), DOI 10.1007/978-3-030-79876-5_37.
  • The mathlib Community, "The Lean mathematical library", CPP 2020, DOI 10.1145/3372885.3373824.
  • J. Tooby-Smith and contributors, physlib, the community Lean 4 physics library (the successor of PhysLean), Apache 2.0, github.com/leanprover-community/physlib. The library carries no DOI of its own, so it is cited by name and URL.

What the map takes from a code

A representation records interface facts (keywords, file formats, units), citations, and published equations, written in our own words. The map does not vendor or copy any code's source, so no code's license applies to this repository: the kernel is Apache 2.0 and the map data is CC BY 4.0. Copyleft codes, such as GPUMD under GPL-3.0, are cited and described the same way as permissively licensed ones. The GPL does not restrict describing an interface for interoperability or citing a paper.

Running a code remains under that code's own license, on the side of whoever runs it. Each recorded license comes from the code's own LICENSE file, and a DOI is recorded only when one can be verified.