Lean 4.28.0 is out! New symbolic simulation framework for 𝚐𝚛𝚒𝚗𝚍, user-defined 𝚐𝚛𝚒𝚗𝚍 attributes for custom tactics, a new 𝚜𝚘𝚕𝚟𝚎𝚛𝙼𝚘𝚍𝚎 in 𝚋𝚟_𝚍𝚎𝚌𝚒𝚍𝚎 for proof vs. counterexample search, and lean4checker available out of the box.

lean-lang.org/doc/referenc...

#LeanLang #LeanProver #ProofAssistant

50 years of proof assistants
lawrencecpaulson.github.io//2025/12/05/History_of_P...

#ProofAssistant #Isabelle #Coq #Rocq #LCF #HOL

Tactic tip: Lean's 𝚜𝚒𝚖𝚙? is an optimization tool that shows the minimal 𝚜𝚒𝚖𝚙 𝚘𝚗𝚕𝚢 call needed to close a goal.

Use the 𝚜𝚒𝚖𝚙? "Try this" suggestion to insert the precise 𝚜𝚒𝚖𝚙 𝚘𝚗𝚕𝚢 call into your proof.

Learn more: lean-lang.org/theorem_prov...

#LeanLang #LeanProver #ProofAssistant

Pelletier’s Problem 24 in Mizar There are probably several different ways to prove Pelletier’s Problem 24, so we will just investigate one way. Informal Roadmap for the Proof The first thing to do, whenever formalizing anyt…

I worked through one possible solution to proving Pelletier's problem 24 in the #Mizar #proofassistant, but there are others.

thmprover.wordpress.com/2025/10/19/p...

Schemas and Proofs: A worked example Today, we will work through proving one of Pelletier’s Seventy Five Problems for Testing Automated Theorem Provers. The focus will be on the proof of the claim. Then we will give several &#82…

Despite the tornados and thunder storms, I wrote a brief "worked example" of how to prove one of Pelletier's problems in the #Mizar #proofassistant.

This is part of the "Mizar 101" series of posts.

thmprover.wordpress.com/2025/10/14/s...

How to check you installed Mizar correctly We will be starting a “Mizar 101” series of posts, which will focus on “first steps in Mizar”. This post will discuss, among other things, “How to check you installed …

I've started a "Mizar 101" series of posts oriented towards people who have just installed the #Mizar #proofassistant, but don't really know what to do from there.

The first thing to check is that you installed Mizar correctly, that it "works".

thmprover.wordpress.com/2025/10/11/h...

Literate Implementations of Proof Assistants I have been experimenting with literate programming applied to the implementation of a toy HOL, and transcribing the Mizar proof assistant into Knuth’s WEB. This post will be more “prog…

I wrote a little about "literate programming" used to implement proof assistants, mostly about the "literate programming".

#LiterateProgramming #ProofAssistant #Logic #Mathematics

thmprover.wordpress.com/2025/09/16/l...

Readings shared August 1, 2025 The readings shared in Bluesky on 1 August 2025 are Unconstrained optimization (in Isabelle/HOL). ~ Dustin Bryant. #ITP #IsabelleHOL #Math Seed-Prover: Deep and broad reasoning for automated theorem

Readings shared August 1, 2025. jaalonso.github.io/vestigium/po... #Haskell #LeanProver #Math #ProofAssistant

Readings shared July 31, 2025 The readings shared in Bluesky on 31 July 2025 are The math is haunted. ~ Dan Abramov. #ProofAssistant #LeanProver #Math #Exercitium: Problemas de programación con Haskell (julio de 2018). #Haskell #

Readings shared July 31, 2025. jaalonso.github.io/vestigium/po... FunctionalProgramming #Haskell #LeanProver #Math #ProofAssistant

The Math Is Haunted — overreacted A taste of Lean.

The math is haunted. ~ Dan Abramov. overreacted.io/the-math-is-... #ProofAssistant #LeanProver #Math

Universal Pairs for Diophantine Equations Universal Pairs for Diophantine Equations in the Archive of Formal Proofs

Universal pairs for diophantine equations (in Isabelle/HOL). ~ Marco David et als. www.isa-afp.org/entries/Diop... #ITP #ProofAssistant #IsabelleHOL #Math

Readings shared July 29, 2025 The readings shared in Bluesky on 29 July 2025 are Algorithmic conversion with surjective pairing: A syntactic and untyped approach. ~ Yiyun Liu, Stephanie Weirich. #FormalVerification #ProofAssistan

Readings shared July 29, 2025. jaalonso.github.io/vestigium/po... #CoqProver #FormalVerification #FunctionalProgramming #Haskell #IMO #ITP #LLMs #LeanProver #MachineLearning #Math #ProofAssistant #Rocq #Rust

GitHub - harmonic-ai/IMO2025 Contribute to harmonic-ai/IMO2025 development by creating an account on GitHub.

Harmonic's IMO 2025 results (Harmonic's model Aristotle achieved gold medal performance, solving 5 problems). github.com/harmonic-ai/... #FormalVerification #ProofAssistant #LeanProver #LLMs #Math #IMO

Readings shared July 28, 2025 The readings shared in Bluesky on 28 July 2025 are Gödel's first incompleteness theorem (in Lean4). #FormalVerification #ProofAssistant #LeanProver #Logic #Math Formalized formal logic (in Lean4). #F

Readings shared July 28, 2025. jaalonso.github.io/vestigium/po... #FormalVerification #FunctionalProgramming #Haskell #LeanProver #Logic #Math #ProofAssistant

Formalized formal logic (in Lean4). formalizedformallogic.github.io/Book/ #FormalVerification #ProofAssistant #LeanProver #Logic #Math

Gödel's first incompleteness theorem (in Lean4). formalizedformallogic.github.io/Book/first_o... #FormalVerification #ProofAssistant #LeanProver #Logic #Math

Encoding finite state automata in Agda using coinduction (Evaluating the support for coinduction in Agda). ~ Noky Soekarman. repository.tudelft.nl/file/File_56... #FormalVerification #ProofAssistant #Agda

Modelling cyclic structures in Agda (Evaluating Agda’s coinduction through modelling graphs). ~ Faizel Mangroe. repository.tudelft.nl/file/File_64... #ProofAssistant #Agda

Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL We give an overview of our formalizations in the proof assistant Isabelle/HOL of certain irrationality and transcendence criteria for infinite series from three different research papers: by Erdős and Straus, Hančl, and Hančl and Rucki. Our formalizations in Isabelle/HOL can be found on the Archive of Formal Proofs. Here we describe selected aspects of the formalization and discuss what this reveals about the use and potential of Isabelle/HOL in formalizing modern mathematical research, particularly in these parts of number theory and analysis.

"Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL" by Angeliki Koutsoukou-Argyraki, Wenda Li, and Lawrence Paulson. #ExperimentalMath #ProofAssistant #MathSky

Hey #quantum people! Are you using #lean? Are you using another theorem prover or proof assistant? What are you using it for? Papers and source repos are especially appreciated.
#automatedreasoning #proofassistant #ai1.0 #quantumcomputing

Formalizing Ordinal Partition Relations Using Isabelle/HOL This is an overview of a formalization project in the proof assistant Isabelle/HOL of a number of research results in infinitary combinatorics and set theory (more specifically in ordinal partition relations) by Erdős–Milner, Specker, Larson and Nash-Williams, leading to Larson’s proof of the unpublished result by E.C. Milner asserting that for all m \in\mathbb{N}, \omega^\omega \rightarrow (\omega^\omega,m). This material has been recently formalised by Paulson and is available on the Archive of Formal Proofs; here we discuss some of the most challenging aspects of the formalization process. This project is also a demonstration of working with Zermelo–Fraenkel set theory in higher-order logic.

"Formalizing Ordinal Partition Relations Using Isabelle/HOL" by Mirna Džamonja, Angeliki Koutsoukou-Argyraki, and Lawrence Paulson. #ExperimentalMath #ProofAssistant #MathSky

Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types Church’s simple type theory is often deemed too simple for elaborate mathematical constructions. In particular, doubts were raised whether schemes could be formalized in this setting and a challenge was issued. Schemes are sophisticated mathematical objects in algebraic geometry introduced by Alexander Grothendieck in 1960. In this article we report on a successful formalization of schemes in the simple type theory of the proof assistant Isabelle/HOL, and we discuss the design choices which make this work possible. We show in the particular case of schemes how the powerful dependent types of Coq or Lean can be traded for a minimalist apparatus called locales.

"Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types" by Anthony Bordg, Lawrence Paulson, and Wenda Li. #ExperimentalMath #Lean #AlgebraicGeometry #ProofAssistant #MathSky

Terry Tao has mad some progress on developing a proof assistant for asymptotic analysis
#mathematics #math #AsymptoticAnalysis #ProofAssistant.
Source: buff.ly/pEuagHN

Xena Mathematicians learning Lean by doing.

Also be sure to check the @xenaproject.bsky.social blog to learn more about #Lean #ProofAssistant #MachineLearning #LLM The potential to revolutionise how we do #Math is phenominal.
xenaproject.wordpress.com

Building the Mathematical Library of the Future A small community of mathematicians is using a software program called Lean to build a new digital repository. They hope it represents the future of their field.

@quantamagazine.bsky.social published a nice article on #Lean #ProofAssistant
www.quantamagazine.org/building-the...

Schemes in Lean We tell the story of how schemes were formalized in three different ways in the Lean theorem prover.

"Schemes in Lean" by Kevin Buzzard @xenaproject.bsky.social , Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Fernández, and Scott Morrison. #ExperimentalMath #Lean #ProofAssistant #MathSky

book cover - maths proofs in lean first steps

if you think writing #maths proofs in code is only for PhDs ...

.. this cause was designed just for you!

* small bite-size examples
* concepts over code
* easy exercises to build confidence

www.amazon.com/dp/B0DWHS1RDJ

#mathematics #lean #lean4 #proofassistant

[Not actually true]

Fun fact: they wanted to rename the Coq proof assistant to "glocq", but since the username was already taken on mathstodon they settled on "rocq" instead.

#coq #proofAssistant #formalMethods

Formalize the Octonions Project Summary: Formalize the Octonions in the same spirit as the Reals, Complex, and Quaternions. Earlier work in Mizar. The Cayley-Dickson construction has been formalized in Mizar in the CAYLDI…

Want to formalize something in the #Mizar #proofassistant?

Formalize the #Octonions!

I have sketched out what this would look like, and relate it to pre-existing formalizations in Mizar.

thmprover.wordpress.com/2024/12/19/f...