Readings shared June 21, 2026

The readings shared in Bluesky on 21 June 2026 are: A Lean 4 formalization of euclidean domain algorithms from a 1986 icon experimentation package. ~ Lars Warren Ericson. #LeanProver #ITP #Math A Lea

A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness

The standard convex-algebra interchange axiom, common to probability-monad formalisations since Stone, is provably too weak to support full Bayesian conditioning. We make this precise in Cubical Agda: finite distributions as a higher inductive type, conditional independence as a cubical path between kernels, recursive Bayesian conditioning as a total function on a full-support fragment. Lifting conditioning to the full HIT exposes a structural mismatch -- the two halves of the rearranged 4-leaf mix carry distinct Bayesian weights related by Bayes' formula, not the single shared inner weight the standard axiom provides. We exhibit the minimal generalisation that resolves this and prove the standard form is the degenerate case where the two inner weights coincide. Around this observation we verify the algebraic context constructively, with zero postulates above an abstract ordered-field interface: bind commutativity, the four semi-graphoid axioms, intersection (reduced to contraction via structural $Σ$-witnesses, without positivity), Pearl's do-calculus Rules~1, 2, and~3 in kernel form, finite-type Bayesian conditioning, and Pearl's d-separation theorem (soundness) on arbitrary $n$-vertex finite directed acyclic graphs (DAGs) in both interventional and Bayesian forms. The probability monad is also verified as a Markov category; the abstract interface discharges at $Q$.

Patrik Jansson - Blog posts

BFPG Hack Day - June 2026 · Luma

Come to BFPG Hack Day for some wholesome fun hacking on side projects, tackling tutorials, grinding axes and shaving yaks! Work together or independently.…

Auto formalisation of Chaitin and of the surprise incompleteness Theorem

This is a continuation of a previous report on an experiment in autoformalisation of Gödel's second incompleteness theorem in Agda using Claude. Using the framework built in this experiment, Claude could ``automformalise'' Chaitin's proof of the first incompleteness theorem and then the Kritchman-Raz surprise examination paradox version of the second incompleteness. As the first experiment, the project provides a case study of the strengths and limitations of current large language models in mathematics. Since Chaitin's proof involves coding programs, Claude had to represent code as ternary string and could build autonomously a parser and a continuation stack evaluation machine. The fact that we can simulate computations as expected is not completely trivial and we suggested a Gandy/Howard majorisation argument, that Claude had no problem to follow. The resulting formalisation clarifies a number of details left implicit in the original presentation and provides a fully machine-checked proof of these arguments for Church's Basic Recursive Arithmetic.

Readings shared June 5, 2026

The readings shared in Bluesky on 5 June 2026 are: A formal proof of the Ramanujan-Nagell theorem in Lean 4. ~ Barinder S. Banwait. #LeanProver #ITP #AI4Math Certificate-based verification of derivat

Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic

We report an experiment in autoformalisation of Gödel's second incompleteness theorem in Agda using Claude. The theorem is formalised for Church's Basic Recursive Arithmetic (BRA), following the proof outline given in Guard's 1963 lecture notes. The entire Agda development, comprising approximately 50,000 lines and containing no postulates, was produced through interaction with Claude; the author did not write any Agda code. Beyond the formalisation itself, the project provides a case study of the strengths and limitations of current large language models in mathematics. An initial autonomous attempt based on a theorem of Rose failed because the theorem is false; the resulting formal development produced by Claude established a statement superficially resembling Gödel's theorem but mathematically unrelated to it. This failure was traced to an insufficient specification of the internal provability predicate, illustrating how an LLM may reason correctly from an incorrect formal specification. The final development follows Guard's proof and required the reconstruction of several implicit mathematical arguments, including the role of the internal numeral-encoding operation and the interaction between substitution and numeral closure. The resulting formalisation clarifies a number of details left implicit in the original presentation and provides a fully machine-checked proof of Gödel's second incompleteness theorem for BRA.

A Fully Machine-Checked Formalization of Semisimplicial Types in Agda: Verified via RStudio and Continuous Integration

This report documents the definitive formal verification of the PSIU Protocol using Agda. By implementing a strict semisimplicial universe without Axiom K, we resolve the higher-dimensional coherence challenges (X3 tetrahedral level), ensuring total stability and well typedness of the system. The development of this protocol involved a critical refactoring phase. Previous iterations contained imprecisions in the mapping of higher-order coherences between X2 and X3. These were resolved within a 24-hour sprint by rewriting the core transition formulas, leading to the current verified state. The PSIU Protocol successfully achieves ”Crystallized” stability. The proof is automated via CI/CD and is HoTT-compliant, marking a definitive step in verified semisimplicial structures.   This repository provides a complete formalization of semisimplicial types using Agda, orchestrated through RStudio and validated via GitHub Actions. To ensure the integrity and authenticity of the source files, the entire dataset has been digitally signed using ArubaSign. Usage License: This work is provided exclusively for dissertation and study purposes. Any other use, including commercial exploitation or redistribution without explicit authorization, is strictly prohibited. [email protected] https://github.com/lombardisedr-dev/PsiU-Protocol-HoTT

Readings shared May 4, 2026

The readings shared in Bluesky on 4 May 2026 are: Compfiles: Catalog of math problems formalized in Lean. ~ David Renshaw et als. #LeanProver #ITP #Math Primitive pythagorean triples in lean and redu