Mastodawn

Formalization is not just about proving. It is about understanding, communicating, and building trust at a scale beyond our cognitive abilities." #LeanLang

Adolfo Neto Apr 28

Lean: Extensible, Scalable, Trusted. Slides by Leonardo de Moura Paris, 2026 #LeanLang #LeanProver leodemoura.github.io/static/paris...

Lean: Extensible, Scalable, Tr...

Lean: Extensible, Scalable, Trusted.

Adolfo Neto Apr 23

𝗠𝗮𝘁𝗵𝘀 𝗣𝗿𝗼𝗼𝗳𝘀 𝗶𝗻 𝗟𝗲𝗮𝗻 - 𝗙𝗶𝗿𝘀𝘁 𝗦𝘁𝗲𝗽𝘀 #LeanLang mathstodon.xyz/@rzeta0/1164...

Tariq (@[email protected])

Tariq (@[email protected])

Attached: 2 images 𝗠𝗮𝘁𝗵𝘀 𝗣𝗿𝗼𝗼𝗳𝘀 𝗶𝗻 𝗟𝗲𝗮𝗻 - 𝗙𝗶𝗿𝘀𝘁 𝗦𝘁𝗲𝗽𝘀 You don't need to be a PhD to write simple maths proofs in Lean. This course takes you from a complete beginner, and gives you enough confidence to read and write simple proofs. Each chapter has one exercise, designed to build confidence, not destroy it! youtube: https://www.youtube.com/@LeanFirstSteps/videos free content: https://leanfirststeps.blogspot.com/p/contents.html book: https://www.amazon.com/dp/B0DWHS1RDJ #leanprover #education #maths

Mathstodon

Adolfo Neto Apr 20

Signal Shot is a public moonshot to verify the Signal protocol and its Rust implementation using Lean. Not the math on paper. The actual code. #LeanLang leodemoura.github.io/blog/2026-4-...

Signal Shot: The Platform Is R...

Signal Shot: The Platform Is Ready — Leonardo de Moura

Leonardo de Moura — Creator of Lean and Z3

Lean Apr 20

"Can we prove that Signal's cryptography is secure — not just on paper, but in actual code?"

Signal Shot, launched today at the Software Verification in Lean workshop in Paris, is a public moonshot to formally verify the Signal protocol and its Rust implementation using Lean. A joint effort of Signal, the Beneficial AI Foundation, and the Lean FRO.

Open to contributions from anyone working on software verification, cryptography, protocol design, Rust, or Lean.

🔗 https://www.beneficialaifoundation.org/signal-shot

#leanlang #leanprover #softwareverification #baif #signal

Signal Shot — Beneficial AI Foundation

Beneficial AI Foundation

Lean Apr 2

Lean 4.29.0 released with 453 changes.

Highlights: reduced startup time through static initialization of closed terms, simpler 𝚗𝚘𝚗𝚌𝚘𝚖𝚙𝚞𝚝𝚊𝚋𝚕𝚎 semantics improving predictability, higher-order Miller pattern support in 𝚐𝚛𝚒𝚗𝚍's e-matching engine, and a significant overhaul to instance and reducibility handling.

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

#LeanLang #LeanProver #FormalMethods

Adolfo Neto Mar 21

"ZK proofs are headed for real-world deployment — but writing correct ZK statements is tricky.

Our new post by James Parker introduces zkLean, a Lean library that defines a domain specific language for specifying and formally verifying ZK statements."
#LeanLang

https://www.galois.com/articles/zklean-a-dsl-for-zk-statement-verification