José A. AlonsoEverything you know is wrong. ~ Lawrence Paulson. https://lawrencecpaulson.github.io/2025/09/20/Wrong.html #AI #Logic #ATP #ITP #FunctionalProgramming #LogicProgramming #FormalVerification
An introduction to formal real analysis (Lecture 5: Doubling a convergent sequence). ~ Alex Kontorovich. https://youtu.be/MSp48lKUOGY #ITP #LeanProver #Math
Lecture 5, Introduction to Formal Real Analysis, Rutgers University, Prof. Kontorovich, 09/19/2025
An introduction to formal real analysis (Lecture 4: Non-convergence of (-1)^n, triangle inequality). ~ Alex Kontorovich. https://youtu.be/p2Q4Vgn0QB0 #ITP #LeanProver #Math
Lecture 4, Introduction to Formal Real Analysis, Rutgers University, Prof. Kontorovich, 09/16/2025
Readings shared September 19, 2025. https://jaalonso.github.io/vestigium/posts/2025/09/20-readings_shared_09-19-25 #Agda #CoqProver #ITP #Idris2 #LeanProver #Rocq
Mechanizing the meta-theory of session types in Rocq: A tutorial. ~ Marco Carbone, Alberto Momigliano. https://momigliano.di.unimi.it/papers/stutorial.pdf #ITP #Rocq
The conatural numbers form an exponential commutative semiring. ~ Szumi Xie, Viktor Bense. https://szumixie.github.io/docs/papers/the-conatural-numbers-form-an-exponential-commutative-semiring.pdf #ITP #Agda
Simons Foundation Lean Workshop. ~ Antoine Chambert-Loir. Alex Kontorovich, Heather MacBeth. https://leanprover-community.github.io/blog/posts/simons-lean-workshop/ #ITP #LeanProver
The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction. ~ Arnaud Mayeux, Jujian Zhang. https://arxiv.org/abs/2509.15116 #ITP #LeanProver
Theorem provers: One size fits all? ~ Harrison Oates, Hyeonggeun Yun, Nikhila Gurusinghe. https://arxiv.org/abs/2509.15015 #ITP #CoqProver #Idris2
Theorem Provers: One Size Fits All?
Theorem provers are important tools for people working in formal verification. There are a myriad of interactive systems available today, with varying features and approaches motivating their development. These design choices impact their usability, alongside the problem domain in which they are employed. We test-drive two such provers, Coq and Idris2, by proving the correctness of insertion sort, before providing a qualitative evaluation of their performance. We then compare their community and library support. This work helps users to make an informed choice of system, and highlight approaches in other systems that developers might find useful.
The groupoid-syntax of type theory is a set. ~ Thorsten Altenkirch, Ambrus Kaposi, Szumi Xie. https://arxiv.org/abs/2509.14988 #ITP #Agda
The Groupoid-syntax of Type Theory is a Set
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, we introduce the concept of a Groupoid Category with Families (GCwF). This framework truncates types at the groupoid level and incorporates coherence equations, providing a natural extension of the CwF framework when starting from a 1-category. We demonstrate that the initial GCwF for a type theory with a base family of sets and Pi-types (groupoid-syntax) is set-truncated. Consequently, this allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models. All constructions in this paper were formalised in Cubical Agda.