^^LEAN. Proof assistant.

wp , https://lean-lang.org/about/

Lean is a proof assistant and a functional programming language.

"LEAN" is jokingly referred to as "Less Employees Are Needed", it's not an acronym, "Lean" is a management philosophy about improving processes, not just cutting staff.

It is based on the calculus of constructions with inductive types.
It is an open-source project hosted on GitHub.

1. https://functional.cafe/@leanprover Official account of the Lean theorem prover and programming language.
2. 2025-05-15 hpodcasts.ox.ac.uk/formalizing-future-leans-impact-mathematics-programming-and-ai?video=1
   1. Math is now data that can be processed, transformed and inspected in various ways.
   2. Testing can only show the presence of the bugs, not the absence. - Edsger Wybe Dijkstra
   3. 2025-05-15 https://podcasts.ox.ac.uk/will-computers-prove-theorems?video=1
      1. What's math about? proving or underrstanding theorems? Do we just want to get the job done or do we want to understand whati's happening?
      2. This is this, is very, very wishy washy on exactly how this proof worked.
      3. Language models instead of cognition they are doing recognition. 
3. yt Terence Tao - Machine-Assisted Proofs (February 19, 2025)

Autoformalization in LEAN is harder than autoinformalization.

LEAN to English is a lot easier than English to LEAN, because model has not seen much LEAN.  yt/?si=-4grRBWdpKafQQzz&t=1789

axiommath.ai 

https://axiommath.ai/territory/building-the-reasoning-engine-at-axiom Francois Charton & Alberto Alfarano

Book: The Mechanics of Proof

https://hrmacbeth.github.io/math2001/

This is a book dealing with how to write careful, rigorous mathematical proofs.

From the preface

Interactive theorem-proving systems such as Lean have become steadily easier to use over the years, but they are not yet actually easy to use: they can be fussy and unforgiving, just like any other computer programming language. So why does this book propose that you use such a system in your first encounter with proofs?

The main novelty of this text is the “bilingual” presentation, juxtaposing prose mathematics with Lean code. But the design choices enforced by this presentation have shaped the text in other ways.

Links

1. Proof system.
2. Proof assistant. La matematica in linguaggio informatico.
3. AI matematica.

Links inet

1. wp/Natural_deduction
2. https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/