Exploration: Formalization, Computation, and the Path to Formal Proofs

Status: Exploration. Investigates three converging threads: (1) the formal equivalence between the resonance exchange picture and QFT propagators, (2) the methodology as a computable Bayesian network on a product lattice, and (3) Lean 4 as the tool for translating the methodology and its findings into machine-verified formal mathematics.

Builds on: exploration-locality-information-and-resonant-propagation.md (locality structure, resonance exchange, methodology parallel), analysis-planck-information-substrate.md (6 primitives, SSA topology), the convergence domain analysis, and the complete methodology (methodology.md)

Part I: Resonance Exchange IS the QFT Propagator

1.1 The exact mathematical relationship

The previous exploration proposed that the "resonance exchange" between two structures on the Planck lattice might be formally equivalent to the QFT propagator. Research confirms: they are the same mathematical object.

The connection is the Schwinger proper-time representation. For an operator F = D² + m² (Dirac operator squared plus mass), the Euclidean Green's function (propagator) is:

G(x,y) = ⟨x| F⁻¹ |y⟩ = ∫₀^∞ ds K(x,y,s)

where K(x,y,s) = ⟨x| e^{-sF} |y⟩ is the heat kernel — the amplitude for a disturbance at x to propagate to y in "proper time" s. The propagator IS the time-integrated heat kernel. Not approximately — exactly (up to UV regularization at s→0).

The Feynman propagator (the physical, causal one) is obtained by Wick rotation:

G_F(x,y) = i ∫₀^∞ ds ⟨x| e^{-is(D² + m² - iε)} |y⟩

The heat kernel has a well-known asymptotic expansion:

K(x,y,s) ~ (4πs)^{-d/2} exp(-|x-y|²/4s) Σₙ aₙ(x,y) sⁿ

where aₙ are the Seeley-DeWitt coefficients encoding local geometry. These are the SAME coefficients that appear in the spectral action:

Tr(f(D/Λ)) ~ Λ⁴ f₄ a₀ + Λ² f₂ a₂ + f₀ a₄ + O(Λ⁻²)

The spectral action's heat kernel coefficients determine the propagator's short-distance behavior. a₀ (cosmological constant) controls the vacuum energy. a₂ (Einstein-Hilbert) controls gravitational propagation. a₄ (Yang-Mills + Higgs) controls gauge field and scalar propagation. The spectral action IS the generating functional for all propagators.

1.2 The QCA propagator: the discrete version

In the QCA framework, the discrete propagator is:

G_QCA(x,t; x',t') = ⟨x| U^{t-t'} |x'⟩    (for t > t')

where U is the QCA update rule (a unitary operator on the lattice). This is literally the amplitude of cell x's update propagating to cell x' after (t-t') time steps.

In the resonance exchange picture from the previous exploration:

• Cell x runs D, producing an updated state
• That update propagates through the lattice
• After (t-t') Planck time steps, the update arrives at x'
• The AMPLITUDE of this arrival IS G_QCA(x,t; x',t')

The resonance exchange amplitude IS the QCA propagator. Not metaphorically — literally the same mathematical quantity.

In the continuum limit (lattice spacing ε→0, time steps δt→0, δt/ε = const), the QCA propagator converges to the continuum Dirac propagator. This has been verified for free QED: QCA on a cubic lattice produces the correct continuum propagator (Sellapillay et al., Nature Scientific Reports 2022).

1.3 The S-matrix from resonance exchange

The S-matrix (full scattering amplitudes) derives from propagators via the LSZ reduction formula:

⟨f|S|i⟩ = ∏(external legs) ∫ d⁴xⱼ e^{ip·x} (□ + m²) ... ⟨0|T{φ(x₁)...φ(xₙ)}|0⟩

The time-ordered correlation functions decompose via Feynman diagrams into products of propagators G_F(xᵢ, xⱼ) (internal lines) and vertex factors (from interaction terms).

In the resonance exchange picture: each Feynman diagram IS a specific topology of resonance exchange paths through the lattice. The internal lines are resonance exchange amplitudes between lattice sites. The vertices are points where multiple resonance paths meet and interfere. The S-matrix is the sum over ALL such topologies — every way that the incoming resonance patterns can exchange through the lattice and produce outgoing patterns.

On a lattice, the same structure holds with lattice propagators. The continuum S-matrix emerges in the ε→0 limit. Recent work (arXiv:2503.14600, 2025) provides exact discrete-to-continuum mappings on finite lattices.

1.4 What this establishes

The resonance exchange picture is NOT a new formulation of physics. It IS standard QFT, expressed in CA vocabulary:

This means: the resonance exchange picture doesn't NEED independent validation. It inherits the validation of QFT itself. The entire apparatus of Feynman diagrams, renormalization, the Standard Model — all of it IS the resonance exchange picture computed in detail.

What the resonance exchange vocabulary ADDS is conceptual clarity about locality: every interaction IS local D-operator updates propagating through the lattice. "Action at a distance" is never needed. "Virtual particles" are not mysterious entities — they're lattice propagation amplitudes between source and sink. The vocabulary change doesn't change the math; it clarifies the physical picture.

Part II: The Methodology as a Computable Bayesian Network

2.1 The product lattice as a Bayesian network

The methodology's product lattice has n primitives (n ≤ 8), each with kᵢ discrete partial levels (kᵢ ≤ 6). The dependency structure is a DAG. This IS a Bayesian network:

P(X₁, ..., Xₙ) = ∏ᵢ P(Xᵢ | Pa(Xᵢ))

where Pa(Xᵢ) are the parents of Xᵢ in the dependency DAG.

For a typical domain (n=6, k=6): the raw state space is 6⁶ = 46,656 positions. But the factored representation stores only Σᵢ kᵢ · ∏_{j∈Pa(i)} kⱼ parameters — exponentially smaller for sparse DAGs (which ours are: most primitives have 0-2 parents).

2.2 The coherent sub-lattice as a constraint satisfaction problem

The coherent sub-lattice (the 12-30% of positions that are structurally valid) IS a constraint satisfaction problem (CSP). Each dependency edge imposes a constraint: "if Xᵢ is at level ≥ p, then Pa(Xᵢ) must be at level ≥ q."

The unification of CSP and Bayesian inference: encode hard constraints as zero-probability factors and soft constraints as non-uniform factors. A single framework — the factor graph — handles both:

P(X) = (1/Z) ∏ₐ fₐ(Xₐ)

where each factor fₐ encodes:

• Hard constraints: fₐ = 0 for forbidden configurations (dependency violations)
• Soft constraints: fₐ ∈ (0,1] encoding preference (physics: thermodynamic favorability, kinetic rates)
• Directional dependencies: factors from conditional probability tables P(Xᵢ | Pa(Xᵢ))

The methodology's "heavy pairs" and "light pairs" become pairwise factors with different coupling strengths. Heavy pairs have strong coupling (high mutual information). Light pairs have weak coupling. This is directly computable.

2.3 Forward-backward algorithm = forward/reverse walks

The methodology's forward walks (from initial position, widening) and reverse walks (from known endpoint, narrowing) are precisely the forward-backward algorithm (Baum-Welch 1972):

• Forward variable: α_t(s) = P(X_t = s, evidence₁:t) — probability of being at state s at time t given all evidence up to t
• Backward variable: β_t(s) = P(evidence_{t+1:T} | X_t = s) — probability of future evidence given state s at time t
• Posterior: P(X_t = s | all evidence) ∝ α_t(s) · β_t(s)

This is EXACTLY the formula from the session summary's probabilistic lattice section:

P_actual(position at t) ∝ P_forward(t) × P_reverse(t)

The build-up sequence defines a chain X₁ → X₂ → ... → Xₙ (the Hasse walk order), and forward-backward computes the posterior distribution over each primitive's level given all constraints. Complexity: O(n · k²).

2.4 The area law analog: mutual information bounded by cut size

For Bayesian networks, the mutual information between sub-networks A and B satisfies:

I(X_A; X_B) ≤ Σ_{i ∈ cut(A,B)} H(Xᵢ)

where the cut is the set of variables with edges crossing the partition. This IS the area law for Bayesian networks: the correlation (mutual information) between two regions is bounded by the "boundary" (number of cut variables), not by the "volume" (total variables in each region).

In the methodology: cross-domain constraint flows through bridge primitives (the interface between domains). The bridge primitive count IS the boundary size. The constraint content flowing through the bridge is bounded by this count. This explains why bridge analyses are always tractable even when the domains themselves are complex — the information bottleneck IS the bridge width.

Preliminary evidence this holds in practice: all domain bridges in the methodology have ~6 primitives (same order as domain primitives). The constraint content that flows across bridges is always bounded by what ~6 bridge primitives can carry. The "area" (bridge width) bounds the "information flow" (cross-domain constraint), not the "volume" (domain complexity).

2.5 Computational tractability

For the methodology's lattice sizes (n ≤ 8, k ≤ 6):

Even brute force is tractable. For these lattice sizes, exact inference is trivially computable. No approximations needed. No sampling. No variational methods. Just enumerate.

Recommendation: Junction tree for precomputation (set up the factored structure once), then O(k^w) per query for individual probability computations. This gives:

• Exact posterior distributions over any primitive's level given evidence
• Exact coherent sub-lattice enumeration
• Exact forward and reverse walk computation
• Exact mutual information between any variable subsets

2.6 What this makes possible

With the Bayesian network formalization:

1. Automated coherent sub-lattice computation. Given a dependency DAG and partial level definitions, automatically enumerate all coherent positions and compute the filter percentage. Currently done by hand — could be computed exactly.

2. Quantitative forward/reverse walks. Instead of qualitative "the distribution narrows," compute exact probability distributions at each walk step. Identify the exact point where the distribution becomes narrow enough to determine a finding.

3. Cross-domain constraint propagation. Given evidence in one domain, automatically compute the posterior distribution in connected domains. "If biology has these primitives at these levels, what does the bridge constrain physics to?"

4. Sensitivity analysis. Which evidence has the most impact on the posterior? Which constraints are load-bearing (removing them significantly widens the distribution) vs decorative (removing them changes little)?

5. Prediction generation. Forward walks from a known current state produce probability distributions over future states. These are quantitative, testable predictions — "the entity system's next state is at position X with probability p."

Part III: Lean 4 as the Formalization Path

3.1 Why Lean 4

The methodology's structures are all discrete, finite, and well-defined: product lattices, partial orders, DAGs, constraint satisfaction, probability distributions, Hasse walks. These are precisely the kind of structures that interactive theorem provers excel at. And the PROOFS we want are the kind theorem provers can deliver: "given this dependency structure, the coherent sub-lattice has exactly these members," "the filter percentage is bounded by X," "this walk is the unique path satisfying these constraints."

Why Lean 4 specifically:

Lean 4 wins on the combination: best lattice + category theory coverage, most accessible for programmers, single language, active community, and existing physics formalization efforts (PhysLib at physlib.io).

3.2 What Mathlib4 already provides

Strong coverage (ready to use):

• Mathlib.Order.Lattice — semilattices, lattices, distributive lattices, complete lattices, product orders, Galois connections
• Mathlib.CategoryTheory.* — categories, functors, natural transformations, adjunctions, limits/colimits, Yoneda, monads, monoidal categories
• Finset, Fintype — finite sets, enumeration, counting
• Linear algebra, inner product spaces, basic spectral theory

Developing coverage (usable with some custom work):

• Mathlib.MeasureTheory.* — sigma-algebras, measures, probability measures, integration, conditional expectation
• Mathlib.Combinatorics.SimpleGraph — simple graphs (would need extension for DAGs)

Not yet available (would need to build):

• Bayesian networks / probabilistic graphical models
• Directed acyclic graphs (explicit DAG type with acyclicity proof)
• Constraint satisfaction
• Belief propagation algorithms
• Heat kernels / spectral geometry (long-term)
• C*-algebras, von Neumann algebras (long-term)

3.3 The formalization plan

A staged approach, building from foundations to applications:

Stage 1: Core Lattice Structures (weeks 1-4)

Define the methodology's fundamental objects in Lean 4:

EntityLattice/
  Basic.lean           -- Primitive, PartialLevel, ProductLattice
  Dependency.lean      -- DependencyDAG, coherence predicate
  Coherence.lean       -- CoherentSubLattice, filter computation
  Walk.lean            -- HasseWalk, BuildUpSequence

What gets formalized:

• A Primitive type with its partial levels as a finite totally-ordered set
• The ProductLattice as the product of n such ordered sets
• The DependencyDAG encoding which primitives depend on which
• The Coherent predicate: a position is coherent iff all dependencies are satisfied
• The CoherentSubLattice: the set of all coherent positions
• The FilterPercentage: |coherent| / |total| as a rational number
• HasseWalk: a sequence of coherent positions where each step adds exactly one primitive

Target theorems:

• The coherent sub-lattice is a sub-lattice (closed under meet and join when they exist)
• The filter percentage is computable from the dependency structure
• A Hasse walk exists iff the dependency DAG is acyclic (which it always is)
• The build-up sequence is unique up to topological sort order of the DAG

Why start here: These are the simplest structures, with the clearest definitions. Every later stage builds on them. And the proofs are straightforward — the main value is having MACHINE-VERIFIED definitions that can't be inconsistent.

Stage 2: Probability and Walks (weeks 5-10)

Add probabilistic structure:

EntityLattice/
  Distribution.lean    -- ProbDist over ProductLattice
  FactorGraph.lean     -- Factor graph encoding hard + soft constraints
  ForwardBackward.lean -- Forward/reverse walks as belief propagation
  MutualInfo.lean      -- Information-theoretic quantities

What gets formalized:

• ProbDist: probability distribution over coherent positions
• Factor graph: factors for hard constraints (dependency), soft constraints (physics), evidence
• Forward variable α_t, backward variable β_t, posterior ∝ α · β
• Mutual information I(X_A; X_B) and the cut bound
• Convergence events: points where the distribution width drops discontinuously

Target theorems:

• The posterior ∝ α · β is a valid probability distribution
• The cut bound: I(X_A; X_B) ≤ Σ_{i ∈ cut} H(Xᵢ) (area law analog)
• Forward walks widen the distribution; reverse walks narrow it; intersection gives the tightest constraint
• The coherent sub-lattice filter percentage bounds the prior entropy

Stage 3: Domain Analysis Automation (weeks 11-16)

Encode the methodology's 12-step domain analysis as a computable pipeline:

EntityLattice/
  Domain.lean          -- Domain type, landscape, primitive extraction
  PairAnalysis.lean    -- Pair enumeration, load classification
  CoreTriad.lean       -- Core triad identification
  Emergent.lean        -- Emergent property prediction from compositions

What gets formalized:

• Given a set of candidate primitives and their three-test validation data, compute the valid primitive set
• Given primitives and their dependencies, automatically compute: pair loads, core triads, load-bearing quads, filter percentage
• Given partial level definitions, compute: phase transitions, attractor positions, the layering trap criterion
• Emergent property prediction: given a composition at specific partial levels, which emergent properties are predicted?

Target theorems:

• Core triad uniqueness conditions (when the core triad is uniquely determined by the pair structure)
• The heavy-pair-ratio invariant: for information substrates, heavy pairs ≈ 47% (prove this follows from the dependency structure class)
• Phase transition identification is decidable (given the partial level structure, phase transitions are computable)

Stage 4: Cross-Domain and Physics (long-term, months 6+)

Extend to cross-domain structures and the physics connection:

EntityLattice/
  Bridge.lean          -- Bridge primitives, cross-domain coupling
  RealizationChain.lean -- Realization edges, the full domain graph
  Convergence.lean     -- Convergence domain as abstract pattern
  SpectralLink.lean    -- Connection to spectral theory (requires operator algebra)

What gets formalized:

• Bridge structures: how two domains connect, the translation rules, constraint propagation across bridges
• The realization chain: the DAG of domains from physics to computing
• The convergence domain: the 6 abstract primitives that recur across all convergence processes
• (Long-term) The connection to spectral theory: the heat kernel, the propagator, the spectral action

3.4 Learning path

For a programmer new to Lean 4:

Phase 1: Language basics (1-2 weeks)

• Functional Programming in Lean (lean-lang.org) — for programmers, covers syntax, types, monads
• Natural Number Game (browser-based, interactive) — builds intuition for proving

Phase 2: Proof writing (2-4 weeks)

• Mathematics in Lean by Avigad & Massot — how to formalize math
• Work through examples: prove basic lattice properties, define small product lattices
• Learn Mathlib4's API: Finset, Fintype, Order.Lattice

Phase 3: Building the project (ongoing)

• Start with Stage 1 definitions (the simplest structures)
• Each definition should be TESTED by computing specific instances (e.g., the entity system's 6 primitives)
• Lean 4 allows mixing computation and proof — define the lattice, compute the filter percentage, PROVE it matches the hand-computed value

3.5 Project structure

entity-lattice-formal/
  lakefile.lean                  -- Build config, Mathlib4 dependency
  lean-toolchain                 -- Pinned Lean version
  EntityLattice/
    Basic.lean                   -- Core types: Primitive, Level, ProductLattice
    Dependency.lean              -- DAG, dependency predicate
    Coherence.lean               -- Coherent sub-lattice, filter
    Walk.lean                    -- Hasse walks, build-up sequences
    Probability/
      Distribution.lean          -- Probability distributions
      FactorGraph.lean           -- Factor graph encoding
      ForwardBackward.lean       -- Walk algorithms
      Information.lean           -- Mutual information, entropy
    Domain/
      Analysis.lean              -- 12-step pipeline types
      PairLoad.lean              -- Pair enumeration, load classification
      CoreTriad.lean             -- Core triad computation
      Emergent.lean              -- Emergent property prediction
    Instances/
      EntitySystem.lean          -- The entity system's 6 primitives as a concrete instance
      Biology.lean               -- Biology's 6 primitives
      DiracSubstrate.lean        -- Physics's 6 primitives
      ConvergenceDomain.lean     -- The abstract convergence domain
  Test/
    EntitySystemTest.lean        -- Verify computed results match hand analysis
    BiologyTest.lean
    FilterTest.lean              -- Check filter percentages

Each Instances/ file provides a concrete instantiation of the abstract framework, and the Test/ files verify that the computed results (coherent sub-lattice, filter percentage, core triad, etc.) match the values from the hand analysis. If they match: the hand analysis is machine-verified. If they don't: we've found an error, either in the formalization or in the hand analysis.

Part IV: The Translation Map

4.1 What translates directly

4.2 What requires new formalization

Some concepts from the methodology don't have direct mathematical precedent and would need to be formalized from scratch:

The SSA (Self-Sustaining Arrangement): A domain whose primitives satisfy specific structural relationships: encoding/evaluator/selector roles, feedback cycles, code crystallization. The SSA concept would need a formal definition capturing: (a) the role assignment function (which primitives play which roles), (b) the feedback cycle structure, (c) the crystallization condition.

The convergence domain as an abstract category: The convergence domain's 6 primitives appear across physics, biology, methodology, markets. Formalizing this as a CATEGORY (objects = convergence instances, morphisms = structure-preserving maps between instances) would allow proving: "any system with these 6 primitives instantiated at these levels exhibits these emergent properties."

The evaluation-feedback distance: A structural variable tracking the gap between evaluation and feedback across the realization chain. Currently qualitative (distance ~0 at physics, ~designed max at computing). Formalizing would require: a metric on the realization chain, a definition of "evaluation locus" and "feedback locus," and a proof that the distance increases monotonically along the chain.

Phase transitions between partial levels: Currently identified by inspection ("the phase transition from Cf1→Cf2 is where matter appears"). Formalizing would require: a definition of what CHANGES at a phase transition (some emergent property appears/disappears), and criteria for identifying phase transitions from the lattice structure alone.

4.3 What translates to physics (spectral theory link)

The connection between the methodology's lattice and the physical Planck substrate goes through the propagator equivalence established in Part I:

The deepest parallel: the methodology's forward-backward intersection (P_actual ∝ P_forward × P_reverse) corresponds to the Feynman propagator being the time-ordered product of retarded and advanced propagators. The posterior IS the Feynman propagator on the methodology's lattice. This isn't metaphorical — it's the same mathematical operation (product of forward and backward constraint propagation, normalized) applied to different lattices.

4.4 Formalizing the physics connection in Lean 4

The spectral theory connection is a LONG-TERM goal (Stage 4+). Mathlib4 currently has:

• Inner product spaces and basic spectral theory (spectral theorem for matrices)
• No C*-algebras or von Neumann algebras
• No heat kernel or spectral geometry

The PhysLib project (physlib.io) is building quantum information theory in Lean 4 and has formalized quantum hypothesis testing. Connecting to this work is possible but requires significant mathematical development.

Practical near-term path: formalize the STRUCTURAL parallel (the table above) without formalizing the physics itself. Define a ConvergenceProcess type that captures the shared 6-primitive structure, prove that both the methodology's lattice and the QFT propagator are instances, and derive shared theorems from the abstract type. The physics-SPECIFIC content (D, Hilbert space, spectral action) doesn't need to be formalized to prove the structural theorems — they follow from the convergence domain structure alone.

Part V: Research Directions and Open Questions

5.1 Immediate next steps

1. Set up a Lean 4 project with Mathlib4 dependency. Define the Primitive and ProductLattice types. Encode the entity system's 6 primitives as a concrete instance. Compute the coherent sub-lattice and verify it matches the hand analysis.

2. Implement the Bayesian network in a conventional language (Python with pgmpy, or Julia with BayesNets.jl) as a PROTOTYPE. Use this to: compute exact posteriors for all analyzed domains, generate the filter percentages automatically, run forward/reverse walks numerically, compute mutual information across bridges.

3. Write the factor graph specification for the entity system domain, the biology domain, and the Planck substrate domain. This is the translation step: converting the narrative domain analyses into formal factor graph definitions.

5.2 Medium-term research

4. The convergence domain as a formal category. Define objects (convergence instances: QM, evolution, Bayesian inference, lattice walk, ...), morphisms (structure-preserving maps), and prove: shared theorems (bimodal temporality, distribution narrowing, crystallization conditions) follow from the categorical structure.

5. Quantitative predictions from the Bayesian network. Once the factor graph is formalized: What predictions does the posterior generate? For example: given biology's known primitive levels, what does the bridge to cognition constrain the cognition domain's primitive levels to? These are TESTABLE structural predictions.

6. The area law analog: rigorous statement and proof. Conjecture: for the methodology's lattice, the mutual information between two domains connected by a bridge is bounded by Σ_{b ∈ bridge} H(b). Prove this from the factor graph structure. If true, this is a new structural theorem about information-carrying lattices.

5.3 Long-term goals

7. Machine-verified domain analyses. Every domain analysis (entity system, biology, physics, cognition, convergence domain) encoded as a Lean 4 instance. Every claimed structural property (filter percentage, core triad, heavy pair ratio) machine-verified. Any inconsistency between analyses automatically detected.

8. The heat kernel connection formalized. Given sufficient Lean 4 spectral theory, prove: the methodology's forward-backward walk on the product lattice is structurally isomorphic to the forward-backward propagation of the heat kernel on a spectral triple's Hilbert space. This would be a genuine mathematical theorem connecting the methodology to physics at the level of formal proof.

9. Automated domain analysis. Given a new domain (described as a set of candidate primitives with dependency/landscape data), the Lean 4 system automatically: validates the primitive set, computes the coherent sub-lattice, identifies the core triad, computes the filter percentage, and generates predictions. The analyst provides the domain knowledge; the system provides the structural analysis.

Summary

What we've established

1. The resonance exchange picture IS QFT. The propagator G(x,y) = ∫ ds K(x,y,s) is exactly the resonance exchange amplitude. The S-matrix is the sum over all multi-point exchange topologies. No new physics — new vocabulary for existing physics, with conceptual clarity about locality.

2. The methodology IS a Bayesian network. Product lattice + DAG = Bayesian network. Forward/reverse walks = forward-backward algorithm. Coherent sub-lattice = hard-constraint CSP. Cut bound = area law analog. At our lattice sizes (n≤8, k≤6), exact inference is trivially computable.

3. Lean 4 is the right tool for formalization. Strong lattice theory and category theory in Mathlib4, growing probability theory, most accessible for programmers, existing physics formalization precedent. A staged plan (lattice → probability → domain analysis → physics) builds from simple to complex.

What this makes possible

• Machine-verified structural analysis — no possibility of inconsistency in the formal definitions
• Quantitative predictions — exact posteriors, not qualitative "the distribution narrows"
• Automated analysis — new domains analyzed by the system, not just by hand
• The physics connection as a formal theorem — not just a structural parallel, but a machine-verified mathematical identity

Key references

Propagator/heat kernel:

• Vassilevich, "Heat kernel expansion: user's manual" (hep-th/0306138)
• Chamseddine & Connes, "The Uncanny Precision of the Spectral Action"
• Sellapillay et al., "QED from QCA" (Nature Sci. Rep. 2022)
• arXiv:2503.14600 — discrete-to-continuum propagator mappings

Bayesian networks:

• Pearl (1988), Probabilistic Reasoning in Intelligent Systems
• Kschischang, Frey & Loeliger (2001), "Factor Graphs and the Sum-Product Algorithm"
• Lauritzen & Spiegelhalter (1988), junction tree algorithm
• Dechter (1999), bucket elimination unifying CSP and Bayesian inference

Lean 4:

• Mathlib4: github.com/leanprover-community/mathlib4
• PhysLib (physics in Lean 4): physlib.io
• Mathematics in Lean by Avigad & Massot
• Functional Programming in Lean (lean-lang.org)
• LeanCat benchmark (arXiv:2512.24796)