Pith. sign in

REVIEW 2 major objections 4 minor 32 references

Towards Datalog on Quantum Annealers: Compiling Recursive Logic Programs with Bottom-up Semantics to 2-local Ising Models

T0 review · 2 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read This paper shows that a four-stage compiler turns recursive Datalog programs into 2-local Ising models whose ground state projects exactly onto the program's least Herbrand model, with machine-checked proofs.

desk verdict A competent, honest Datalog-to-Ising compiler with a Lean certificate you cannot currently check; the math looks sound, so review it but force the artifact public. read the letter →

arxiv 2608.04645 v1 pith:KYQEXSJ3 submitted 2026-08-05 cs.PL

Bruno Rucy Carneiro Alves de Lima , Victor Henrique Cabral Pinheiro , Evgenii Dolzhkov , Joseph Haske This is my paper · ORCID
classification cs.PL MSC 68N1768Q6081P68
keywords DatalogQuantumAnnealingIsingModelLogicProgrammingBottom-upEvaluationMinimalMin-OnesSAT2-localHamiltonian
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 tries to close the gap between logic programming and quantum annealers: it gives a four-stage compiler that turns a recursive Datalog program and its input facts into a 2-local Ising Hamiltonian, the kind of energy function an annealing device minimizes. The paper's central claim is that the lowest-energy assignment of the compiled Hamiltonian, projected onto the program's atoms, is exactly the least Herbrand model—the set of facts derivable by bottom-up evaluation. Each rule contributes an energy penalty that is flat on all satisfying assignments and higher on the single violating assignment, while a uniform small cost on every true atom selects the minimal model among all models. Every stage is meant to preserve the minimal model, and the paper reports a machine-checked proof of the overall correspondence. If correct, the result means a well-understood logic-programming semantics can be posed as an energy-minimization problem, and solver failures can be measured against a known optimum rather than a sampler's guess.

What carries the argument

The load-bearing mechanism is the energy gate assigned to each ground rule by Stage 4 of the compiler. A rule $h \leftarrow b_1,\dots,b_k$ has exactly one violating assignment—all body atoms true and the head false—so the encoding makes that assignment strictly more costly than every satisfying assignment while leaving all other assignments at the same floor energy. Three gate shapes cover rules with at most two body atoms: a fact becomes a strong field forcing the head true, a one-body implication becomes a pairwise field-plus-coupling term, and a two-body implication uses one private ancilla spin to express its degree-3 violation as a quadratic term. A uniform field $\eta_f = \varepsilon/2$ on every atom then makes the energy of any model equal to a constant plus $\varepsilon$ times the number of true atoms, so the smallest model—the least Herbrand model—is the unique minimum. The ancilla spins carry no semantic meaning; minimizing them out leaves an energy over atom spins only.

What would settle it

Enumerate all spin assignments of the compiled Hamiltonian for the cyclic program $p \leftarrow q$, $q \leftarrow p$ with empty EDB at the paper's $\varepsilon = 1$, $W = 3$: the paper predicts the empty set has energy $-7$ and $\{p,q\}$ has energy $-5$. Any exact solver that returns $\{p,q\}$ as the ground state refutes the correspondence; reproducing the predicted energies on this instance and on a small nonlinear transitive-closure instance would corroborate the implemented encoding.

Watch

Extended reading notes

Core claim

On the paper's terms, the central discovery is a compiler $I = C_4 \circ C_3 \circ C_2 \circ C_1$ from recursive Datalog programs to 2-local Ising models with the property that every ground state of the compiled Hamiltonian projects onto the least Herbrand model of the source program: for every non-auxiliary ground atom $f$, the spin $\sigma_f$ is $+1$ exactly when $f \in M_P(D)$. The pipeline binarizes rules to at most two body atoms, grounds them to a finite clause set, reads that set as a Min-Ones SAT formula, and encodes each implication as an energy gate that rests at a floor on all satisfying assignments and rises by a gap on the unique violating assignment. A uniform cost of $\varepsilon = 1$ per true atom, with gates scaled by a weight $W$ larger than any possible model size, makes the least model the unique minimizer of the atom-projected energy. The paper reports that the per-stage preservation lemmas, the $\varepsilon$-minimality theorem, the 2-locality of the Hamiltonian, and the overall correspondence theorem are all verified in a machine-checked proof assistant, with the statements reproduced verbatim in an appendix.

Load-bearing premise

The whole guarantee rests on the machine-checked proof being faithful to the prose compiler and free of admitted axioms; the development is not public, so a reader cannot yet confirm that the statements printed in the appendix are the actual verified statements.

Editorial extensions

If this is right

  • Any definite Datalog program with a nonempty Herbrand universe can be posed as an annealing problem whose optimum is known in advance, so solvers can be scored by exact recovery rather than by sampled estimates.
  • Disjunction needs no dedicated construct: two rules sharing a head produce two implication gates on the same head spin, whose conjunction is equivalent to the disjunction of their bodies.
  • On cyclic programs the uniform per-true-atom cost rejects unfounded, self-supporting sets, selecting the minimal model directly without Clark completion or loop formulas.
  • The logical interaction graph of the compiled model becomes denser as recursive rules grow, so embedding onto sparse annealer topologies is a growing overhead; at chip scale the paper measures zero recovery by the simulated solvers it tests.

Reading between the lines

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

  • Going beyond the paper: the same gate-plus-uniform-field construction could be adapted to non-Horn fragments, where minimal-model or answer-set semantics differ, by changing which assignments are penalized; that would test whether energy-based selection generalizes beyond definite programs.
  • Going beyond the paper: because the measured recovery collapse tracks the presence of unfounded self-supporting sets rather than raw instance size, a natural next experiment is to add penalty terms that break those cycles and measure whether simulated annealers then recover the minimal model on the currently failing families.
  • Going beyond the paper: an implicit practical reading is that for tractable Horn programs the compilation is a benchmarking harness, not a speedup—a classical incremental engine solves the largest evaluated instances in milliseconds while both simulated solvers fail on them.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 4 minor

Summary. The paper presents a four-stage compiler from recursive Datalog programs to 2-local Ising Hamiltonians, with the central claim that the ground state of the compiled model projects exactly onto the least Herbrand model of the source program. Stage 1 binarizes rules, Stage 2 grounds to a relevant set of instances, Stage 3 converts the ground program to CNF and reads it as Min-Ones SAT, and Stage 4 builds a 2-local Ising model with a uniform per-true-atom field. The authors provide per-stage correctness lemmas and a final correspondence theorem (Theorem 2), which they claim are verified in Lean 4 and whose statements are reproduced in Appendix A. The paper also reports a reference Python compiler, exact enumeration of all assignments for a small instance, minor-embedding results on Pegasus and Zephyr topologies, and classical SA/SQA recovery experiments showing that recursive programs create unfounded-support local minima that the samplers fail to escape.

Significance. If the verification is sound and the artifact is checkable, this is a valuable contribution: it provides a machine-checked bridge from a declarative logic-programming language to quantum-annealing hardware, and it honestly quantifies where current sampling methods fail on the resulting energy landscapes. The reduction to Min-Ones SAT on Horn formulas is not new, but the explicit staged pipeline with per-stage preservation lemmas and the identification of foundedness traps are useful. The paper's empirical admission that recursive families are not recovered at chip scale while a classical engine answers in milliseconds is a strength in terms of scientific honesty. However, the central theorem's machine-checked certificate is currently inaccessible, and there is a concrete mismatch between the prose Hamiltonian and the formal energy model, so the verification claim cannot yet be fully assessed.

major comments (2)
  1. [§3.4 and Appendix A] The formal energy model is Int-valued while the prose Hamiltonian is half-integer. In §3.4 the uniform field is set to η_f = ε/2 with ε = 1, and Figure 1 reports the minimal-model energy as -1,800.5, a half-integer. Appendix A, however, defines Model.energy : (ι → Spin) → Int and spinVal : Spin → Int. Therefore the Lean statement IsGroundState cannot refer to the same Hamiltonian H; it must be a rescaled version, most plausibly 2H. The paper nowhere states this rescaling, and Theorem 2 is phrased as a correspondence for the prose H. Because a positive rescaling preserves ground states, the theorem could still be sound, but the exact relation between the verified energy and H must be stated, and the preservation of ground states under that scaling must be argued. As written, the verified statement and the reference compiler's energy values may describe different objects.
  2. [§3.5 and Appendix A] The machine-checked certificate is not available for review. The footnote in §3.5 says 'The repository will be made public upon acceptance' and no commit hash is provided. Since Theorem 2 is the central claim and its only certificate is the Lean 4 development, a reader cannot currently verify that C4.pipeline_correct_edb is sorry-free, that #print axioms reports only the three standard axioms, or that the statements printed in Appendix A are the actual verified statements. A public artifact with a commit hash, build instructions, and the exact versions of Lean 4 and mathlib is needed before the verification claim can be checked.
minor comments (4)
  1. [§3.4, Theorem 1 proof] The proof writes 'cost(I) ≥ c0 + W (the physical rise is at least W Δ_min)', but the parenthetical suggests the lower bound should be c0 + W Δ_min, which equals c0 + 4W by Table 1. The weaker bound c0 + W is sufficient for the subsequent inequality, but the text should be made consistent.
  2. [Table 4 and Figure 1] There are formatting issues in the header '200reads of1 ,000sweeps' and in the Figure 1 axis label 'Energy (H)'; these should be cleaned up for the camera-ready version.
  3. [Appendix A, C4.encode] The statement C4.encode concludes an if-and-only-if for all g without an isAux side condition, while C4.pipeline_correct_edb adds the restriction hg : isAux g.pred = false. A brief clarification that C4.encode operates on the already-binarized ground program, where auxiliary predicates are ordinary atoms, would help readers reconcile the two statements.
  4. [§3.4] The notation is slightly inconsistent: Section 2.3 uses σ_f for spins, while Table 1 and the surrounding text use s_x, η_x, and σ_x interchangeably. Please unify the notation.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the ground-state correspondence is proved from an independent specification; the sole self-citation is a non-load-bearing baseline and the artifact gaps are auditability issues, not circular reductions.

full rationale

The derivation is self-contained rather than circular. The specification (least Herbrand model, Section 2.1) and the compiled Hamiltonian (Section 3.4) are defined independently, and Theorem 2's Lean statement C4.pipeline_correct_edb does not assume the conclusion it proves: the ground-state predicate IsGroundState is defined generically, and the theorem relates it to minimalModel P D for arbitrary P and D under the stated size hypotheses. The reduction of a ground Horn program to Min-Ones SAT (Lemma 3) is a standard independent fact, and the uniform field is not fitted: epsilon=1 and W=n_atoms+1 are chosen from the atom count, not from the particular minimal model, and Theorem 1's proof uses only the generic violation gap W times Delta_min and the bound |M_P(D)| <= N < W. No parameter is calibrated to the data whose 'prediction' is then announced. The only self-citation, [31] (PyDBSP), is a classical runtime baseline in Section 4 and carries none of the proof. The paper's own limitations -- footnote 1 that the repository will be made public upon acceptance, Appendix A's omission of the C1.run through C4.run definitions, and the Int-valued formal energy versus the half-integer prose Hamiltonian -- are verification/artifact gaps, not circular reductions; a ground-state-preserving rescaling such as 2H would reconcile the last point. They affect auditability and correctness confidence but do not make any step equivalent to its input by construction.

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

The compiler relies on standard Datalog, Horn-satisfiability, and Ising-encoding results. The only hand-chosen numbers are the gate coefficients, epsilon, and the weight W, which are construction constants rather than fitted parameters. No new physical entities are introduced; auxiliary predicates and ancilla spins are internal compilation variables with fully specified semantics.

free parameters (3)
  • epsilon (uniform per-true-atom cost) = 1
    Chosen to satisfy epsilon*N < W and to make the per-atom cost exactly 1; not fitted to data.
  • global gate weight W = |B_bin| + 1 (deployed)
    Integer scale multiplying all rule-gate energies; chosen so any single violation, costing at least W*Delta_min, dominates the maximum possible cardinality cost epsilon*N. Computed from the ground program size.
  • Gate coefficients (eta,J)
    Hand-chosen integers realizing the energy tables in Table 1, e.g. fact eta=-5, 1-IMPLY eta_b=+1, eta_h=-1, J=-1, and 2-IMPLY eta_z=+1, eta_h=-1, J_lr=+1, J_zl=J_zr=J_zh=-1. They are construction constants, not fitted to data.
assumptions (6)
  • standard math The least Herbrand model of a definite program exists and is the least fixpoint of the monotone immediate-consequence operator (Knaster-Tarski).
    Used in Section 2.1 and Lemma 3 as the definition of Datalog semantics.
  • standard math For Horn CNF formulas, the unique Min-Ones SAT solution is the least model and is computable in linear time.
    Used in Section 3.3 and Lemma 3; the binarized ground program yields Horn clauses.
  • standard math A degree-3 product penalty can be reduced to a 2-local quadratic form using one auxiliary ancilla spin (Rosenberg reduction).
    Used in Section 3.4 for the 2-IMPLY gate.
  • domain assumption Quantum annealers realize 2-local Ising Hamiltonians with programmable fields and couplings, and arbitrary logical graphs can be minor-embedded into sparse hardware graphs.
    Used in Sections 2.3 and 4; motivates the encoding and the embedding experiments.
  • standard math The formal verification uses Lean 4 with the three foundational axioms propext, Classical.choice, and Quot.sound.
    Appendix A states the #print axioms output of the development.
  • domain assumption The correctness theorem is stated for exact rational coefficients; physical device precision is analyzed separately in Section 4.
    Isolates the ideal-model theorem from hardware precision, which the authors quantify.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Towards Datalog on Quantum Annealers: Compiling Recursive Logic Programs with Bottom-up Semantics to 2-local Ising Models." pith.science (2026). https://pith.science/paper/KYQEXSJ3

@misc{pith2026260804645,
  author       = {Pith},
  title        = {Pith review of: Towards Datalog on Quantum Annealers: Compiling Recursive Logic Programs with Bottom-up Semantics to 2-local Ising Models},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/KYQEXSJ3}},
  note         = {Machine review of arXiv:2608.04645}
}
read the original abstract

Quantum annealers solve problems by finding the lowest-energy (ground) state of a programmable physical system, a 2-local Ising model, whose energy function is the Hamiltonian. We compile recursive Datalog programs into such models so that the ground state projects onto the program's minimal Herbrand model. The compiler has four stages: binarization, grounding, reduction to a Min-Ones SAT formula, and Ising encoding. Each rule becomes an energy penalty on the one assignment that violates it, and a small uniform cost on every true atom selects the minimal model. We contribute both in theory and in practice with per-stage correctness lemmas and a correspondence theorem, verified in Lean 4, establishing that the ground state of the compiled model projects onto the program's minimal Herbrand model. We map the compiled models onto the topologies of commercial annealers and characterize, under classical and simulated-quantum annealing, whether and when that certified ground state is attained.

Figures

Figures reproduced from arXiv: 2608.04645 by the authors.

Figure 1
Figure 1. walks through this space. Each position on the horizontal axis is one assignment, consecutive assignments differ in exactly one atom, and the tick label names the atom added at that step, with the curve interpolating between the plotted states. The vertical axis is the assignment’s energy. The walk starts at D, the assignment holding exactly the three Edge facts, which the 0-IMPLY gates force into every low-energy s… view at source ↗
Figure 2
Figure 2. Two independently compiled reachability programs at the shipped machine’s scale. Left: each instance’s EDB, the Zephyr Z1 hardware graph (48 nodes, 280 edges). Right: both compiled programs, 1,778 logical spins, minor-embedded together into the ideal Zephyr Z12 generator (4,800 sites), occupying 3,489 physical qubits with longest chain 36. One instance is green, the other purple, unused qubits are greyed. stored edg… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

32 extracted references · 16 canonical work pages

  1. [1]

    Kadowaki, H

    T. Kadowaki, H. Nishimori, Quantum annealing in the transverse Ising model, Physical Review E 58 (1998) 5355–5363. doi:10.1103/PhysRevE.58.5355

    doi:10.1103/physreve.58.5355 1998

  2. [2]

    M. W. Johnson, et al., Quantum annealing with manufactured spins, Nature 473 (2011) 194–198. doi: 10.1038/nature10012

    doi:10.1038/nature10012 2011

  3. [3]

    Colmerauer, P

    A. Colmerauer, P . Roussel, The birth of Prolog, in: History of Programming Languages—II, ACM, 1996, pp. 331–367. doi:10.1145/234286.1057820

    work page arXiv 1996

  4. [4]

    Ising, Beitrag zur theorie des ferromagnetismus, Zeitschrift für Physik 31 (1925) 253–258

    E. Ising, Beitrag zur theorie des ferromagnetismus, Zeitschrift für Physik 31 (1925) 253–258. doi:10.1007/BF02980577

    doi:10.1007/bf02980577 1925

  5. [5]

    Pakin, Performing fully parallel constraint logic programming on a quantum annealer, Theory and Practice of Logic Programming 18 (2018) 928–949

    S. Pakin, Performing fully parallel constraint logic programming on a quantum annealer, Theory and Practice of Logic Programming 18 (2018) 928–949. doi:10.1017/S1471068418000066

    work page doi:10.1017/s1471068418000066 2018

  6. [6]

    S. Ceri, G. Gottlob, L. Tanca, What you always wanted to know about Datalog (and never dared to ask), IEEE Transactions on Knowledge and Data Engineering 1 (1989) 146–166. doi:10.1109/69.43410

    doi:10.1109/69.43410 1989

  7. [7]

    M. H. van Emden, R. A. Kowalski, The semantics of predicate logic as a programming language, Journal of the ACM 23 (1976) 733–742. doi:10.1145/321978.321991

    work page arXiv 1976

  8. [8]

    de Moura, S

    L. de Moura, S. Ullrich, The Lean 4 theorem prover and programming language, in: Automated Deduction (CADE), volume 12699 ofLecture Notes in Computer Science, Springer, 2021, pp. 625–635. doi:10.1007/978-3-030-79876-5_37

    doi:10.1007/978-3-030-79876-5_37 2021

Show all 32 references
  1. [9]

    Pinkas, Symmetric neural networks and propositional logic satisfiability, Neural Computation 3 (1991) 282–291

    G. Pinkas, Symmetric neural networks and propositional logic satisfiability, Neural Computation 3 (1991) 282–291. doi:10. 1162/neco.1991.3.2.282

    1991

  2. [10]

    W. A. T. Wan Abdullah, Logic programming on a neural network, International Journal of Intelligent Systems 7 (1992) 513–519. doi:10.1002/int.4550070604

    1992 doi

  3. [11]

    Lucas, Ising formulations of many NP problems, Frontiers in Physics 2 (2014) 5

    A. Lucas, Ising formulations of many NP problems, Frontiers in Physics 2 (2014) 5. doi:10.3389/fphy.2014.00005

    2014

  4. [12]

    Z. Bian, F. Chudak, W. Macready, A. Roy, R. Sebastiani, S. Varotti, Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results, Information and Computation 275 (2020) 104609. doi: 10.1016/j.ic.2020. 104609

    2020 doi

  5. [13]

    Gelfond, V

    M. Gelfond, V . Lifschitz, The stable model semantics for logic programming, in: Logic Programming, Proceedings of the Fifth International Conference and Symposium, MIT Press, 1988, pp. 1070–1080

    1988

  6. [14]

    L. K. Grover, A fast quantum mechanical algorithm for database search, in: Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC), 1996, pp. 212–219. doi:10.1145/237814.237866

    1996

  7. [15]

    Romanello, D

    R. Romanello, D. D. Giustina, S. Pessotto, C. Piazza, Speeding up answer set programming by quantum computing, in: Proceedings of the 2024 Workshop on Quantum Search and Information Retrieval, ACM, 2024, pp. 1–8. doi:10.1145/3660318. 3660328

    2024 doi

  8. [16]

    Ben-Eliyahu, R

    R. Ben-Eliyahu, R. Dechter, On computing minimal models, Annals of Mathematics and Artificial Intelligence 18 (1996) 3–27. doi:10.1007/BF02136172

    1996 doi

  9. [17]

    Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics 5 (1955) 285–309

    A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics 5 (1955) 285–309

    1955

  10. [18]

    Abiteboul, R

    S. Abiteboul, R. Hull, V . Vianu, Foundations of Databases, Addison-Wesley, 1995

    1995

  11. [19]

    Boothby, P

    K. Boothby, P . Bunyk, J. Raymond, A. Roy, Next-generation topology of D-Wave quantum processors, arXiv:2003.00133, 2020

    2003 arXiv

  12. [20]

    Boothby, A

    K. Boothby, A. D. King, J. Raymond, Zephyr Topology of D-Wave Quantum Processors, Technical Report 14-1056A-A, D-Wave Systems Inc., 2021

    2021

  13. [21]

    Choi, Minor-embedding in adiabatic quantum computation: I

    V . Choi, Minor-embedding in adiabatic quantum computation: I. the parameter setting problem, Quantum Information Processing 7 (2008) 193–209. doi:10.1007/s11128-008-0082-9

    2008 doi

  14. [22]

    M. Y. Vardi, The complexity of relational query languages, in: Proceedings of the 14th Annual ACM Symposium on Theory of Computing (STOC), 1982, pp. 137–146. doi:10.1145/800070.802186

    1982

  15. [23]

    Bancilhon, D

    F. Bancilhon, D. Maier, Y. Sagiv, J. D. Ullman, Magic sets and other strange ways to implement logic programs, in: Proceedings of the 5th ACM SIGACT-SIGMOD Symposium on Principles of Database Systems (PODS), 1986, pp. 1–15. doi:10.1145/6012.15399

    1986

  16. [24]

    Khanna, M

    S. Khanna, M. Sudan, L. Trevisan, D. P . Williamson, The approximability of constraint satisfaction problems, SIAM Journal on Computing 30 (2001) 1863–1920. doi:10.1137/S0097539799349948

    2001 doi

  17. [25]

    W. F. Dowling, J. H. Gallier, Linear-time algorithms for testing the satisfiability of propositional Horn formulae, The Journal of Logic Programming 1 (1984) 267–284. doi:10.1016/0743-1066(84)90014-1

    1984 doi

  18. [26]

    I. G. Rosenberg, Reduction of bivalent maximization to the quadratic case, Cahiers du Centre d’Études de Recherche Opérationnelle 17 (1975) 71–74

    1975

  19. [27]

    K. L. Clark, Negation as failure, in: H. Gallaire, J. Minker (Eds.), Logic and Data Bases, Plenum Press, New York, 1978, pp. 293–322. doi:10.1007/978-1-4684-3384-5_11

    1978 doi

  20. [28]

    F. Lin, Y. Zhao, ASSAT: Computing answer sets of a logic program by SAT solvers, Artificial Intelligence 157 (2004) 115–137. doi:10.1016/j.artint.2004.04.004

    2004 doi

  21. [29]

    Van Gelder, K

    A. Van Gelder, K. A. Ross, J. S. Schlipf, The well-founded semantics for general logic programs, Journal of the ACM 38 (1991) 619–649. doi:10.1145/116825.116838

    1991

  22. [30]

    A. D. King, et al., Beyond-classical computation in quantum simulation, Science 388 (2025) 199–204. doi: 10.1126/science. ado6285

    2025 doi

  23. [31]

    B. R. C. A. de Lima, K. Apinis, M. Kramer, K. Micinski, Incremental evaluation of dynamic Datalog programs as a higher-order DBSP program, in: Datalog-2.0 2024, volume 3801 ofCEUR Workshop Proceedings, 2024, pp. 2–16

    2024

  24. [32]

    D-Wave Quantum Inc., Integrated control errors (ICE), https://docs.dwavequantum.com, 2026. A. The Verified Statements The statements below are reproducedverbatimfrom the Lean 4 development, generated mechan- ically from the sources, with proofs elided as .... The namespace of ...

    2026

Pith tools

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