José A. Alonso
Auto formalisation of Goedel's second incompleteness theorem in binary recursive arithmetic. ~ Thierry Coquand. https://arxiv.org/abs/2606.01898v1 #AI4Math #Agda #ITP #Logic #Math
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.
Roberto LombardiStructural Refactoring Objectives
https://doi.org/10.5281/zenodo.20138853
https://github.com/lombardisedr-dev/PsiU-Protocol-HoTT/blob/main/README.md
The recent optimization phase was dedicated to three fundamental pillars:Homotopic Formalization: A rigorous, clean, and clear theorization at the formal level, ensuring the \(X_{n}\) hierarchy is logically transparent.Protocol Optimization: The creation of an enhanced version of the PSIU Protocol, including its full integration with YML-based verification (CI/CD) for automated auditing.Comprehensive Reporting: Detailed documentation of results and architectural modifications, providing a traceable path for peer-review and future scalability.
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.
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
Mike MolSo this was funny. My solver rederived theorems that had been marked as private because it predicted they'd be there. Twice. #agda
```
-- Made public 2026-05-02 (Step 1 of orbit-aware-completion-residue
-- arc): NSAHomReal2Complex re-derived `α*0` / `0*α` / `neg-0`
-- inline; Goal-T's `*-comm-ℂ` proof would re-derive them again.
-- Two re-derivations of identical content trigger RFS to expose
-- the originals. Behavior-preserving for existing callers.
```
Delooping generated groups in homotopy type theory. ~ Camil Champin, Samuel Mimram, Emile Oleon. https://arxiv.org/abs/2405.03264v1 #Agda #ITP #HoTT
Delooping generated groups in homotopy type theory
Homotopy type theory is a logical setting based on Martin-Löf type theory in which one can perform geometric constructions and proofs in a synthetic way. Namely, types can be interpreted as spaces (up to continuous deformation) and proofs as homotopy invariant constructions. In this context, the loop spaces of types with a distinguished element (more precisely, pointed connected groupoids), provide a natural representation of groups, what we call here internal groups. The construction which internalizes a given group is called delooping, because it is a formal inverse to the loop space operator. As we recall in the article, this delooping operation has a concrete definition for any group G given by the type of G-torsors. Those are particular sets together with an action of G, which means that they come equipped with an endomorphism for every element of G. We show that, when a generating set is known for the group, we can construct a smaller representation of the type of G-torsors, using the fact that we only need automorphisms for the elements of the generating set. We thus obtain a concise definition of (internal) groups in homotopy type theory, which can be useful to define deloopings without resorting to higher inductive types, or to perform computations on those. We also investigate an abstract construction for the Cayley group of a generated group. Most of the developments performed in the article have been formalized using the cubical version of the Agda proof assistant.
Linotype PilgrimThen the sloppification of the #Agda codebase drove any serious person off Agda.
Mikan proof assistant is an 'ai'-free fork by types.pl/@amy
Amélia Liao (@[email protected])
Amélia Liao (@[email protected])
Amélia Liao (@[email protected])
6.89K Toots, 258 Following, 1.41K Followers · 1Lab main author. Charitably describable as "hinged"
Buridan's procrastinator ⁂Nice, now I can go back to being unproductive with #agda.
{ pkgs ? import <nixpkgs> { } }:
with pkgs;
mkShell {
buildInputs = [
(agda.withPackages (ps: [
ps.standard-library
]))
];
}
Formalizing the real numbers in Homotopy Type Theory with Cubical Agda. ~ Jackson Brough. https://users.cs.utah.edu/~blg/resources/pdf/jackson-brough-cubicalreals-2026.pdf #Agda #ITP #Math