Lean 4.31.0 is released.

This consolidation-heavy release brings 305 changes. For those working on verified software: repeat/while loops are now verifiable without requiring source changes, expanding through whileM to support a one-step unfolding lemma. The new experimental mvcgen' tactic, reimplemented from the ground up on the SymM-based symbolic evaluation framework, can outperform mvcgen by a factor of over 100x on some synthetic benchmarks.

Library authors and package maintainers also gain a built-in linting framework through lake lint, with linters upstreamed from Batteries and Mathlib.

Full release notes: https://lean-lang.org/doc/reference/latest/releases/v4.31.0/

#LeanLang #LeanProver #ProofAssistant #FormalVerification

wtb a proof-assistant named Gnarbunga

https://archive.org/embed/gnarbunga0000brom

#proofassistant #gnarbunga

**Theorem proving with the real numbers**
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-408.html
by John Robert Harrison
November 1996

The author used #HOL to formalise real numbers, including metric, sequences and limits, continuity and differentiation, power series and transcendental functions, integration.

There is also a #CAS and IEEE floating standard verification tools.

#ProofAssistant #Math #FormalVerification #Logic #PLT

50 years of proof assistants
https://lawrencecpaulson.github.io//2025/12/05/History_of_Proof_Assistants.html

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

Functional Data Structures and Algorithms: a Proof Assistant Approach

https://fdsa-book.net/

#HackerNews #FunctionalDataStructures #Algorithms #ProofAssistant #Programming #HN

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

#mathematics #logic #Mizar #proofassistant

https://thmprover.wordpress.com/2025/10/19/pelletiers-problem-24-in-mizar/

Despite the tornados and thunder storms, I wrote a brief "worked example" of how to prove one of Pelletier's problems in Mizar. This is part of the "Mizar 101" series of posts.

#Mizar #proofassistant #logic #mathematics

https://thmprover.wordpress.com/2025/10/14/schemas/

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".

https://thmprover.wordpress.com/2025/10/11/how-to-check-you-installed-mizar-correctly/