#leanlang — Public Fediverse posts

"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

The next bi-monthly #Mathlib community meeting is tomorrow Friday, 13th at 3pm UTC. Join to hear about ongoing #LeanLang formalization projects and connect with other contributors!

➡️ See all upcoming community events on our website: http://lean-lang.org/community/#events

Verified Dynamic Programming with Σ-types in Lean

https://tannerduve.github.io/blog/memoization-sigma/

#HackerNews #Verified #Dynamic #Programming #Σ-types #Lean #DynamicProgramming #LeanLang

The Department of Computer Science, University of Oxford has released recordings of the recent Strachey Series Lectures featuring Leo de Moura and Kevin Buzzard:

1️⃣ "Formalizing the Future: Lean's Impact on Mathematics, Programming, and AI" - Leo de Moura, Chief Architect of Lean

Leo discusses how Lean provides a framework for machine-checkable mathematical proofs and code verification, enabling collaboration between mathematicians, software developers, and AI systems. He also outlines the work the Lean Focused Research Organization does to expand Lean’s capabilities and support the community.

➡️ Watch Leo's lecture here: https://podcasts.ox.ac.uk/formalizing-future-leans-impact-mathematics-programming-and-ai

2️⃣ "Will Computers Prove Theorems?" with Kevin Buzzard, Professor of Mathematics, Imperial College

Kevin examines the potential for AI systems and theorem provers to assist in mathematical discovery, addressing whether computers might someday find patterns in mathematics that humans have missed, and discusses the integration of language models with formal verification systems.

➡️ Watch Kevin's lecture here: https://podcasts.ox.ac.uk/will-computers-prove-theorems

#LeanLang #LeanProver #FormalVerification #Mathematics #AI #TheoremProving #OxfordCS

The Lean FRO team met synchronously in Amsterdam last week for our annual team retreat, and to discuss upcoming work and our Year 3 roadmap! 🇳🇱✨

We had very productive discussions around Lean's future in mathematics, software and hardware verification, and AI for math. It was energizing to see our team's commitment to Lean's continued growth in each of these domains.

We're cooking up many exciting developments that will support both our mathematical community and our growing base of software verification users. Stay tuned for our full Y3 roadmap publication at the end of July!

#LeanLang #LeanProver #Lean4 #FormalVerification #Programming #Mathematics #TheoremProving

Three talks at the recent #ZKProof 7 conference in Sofia caught our attention:

🔹 Alexander Hicks from Ethereum Foundation had some really nice things to say about #LeanLang, calling it "quite a nice functional programming language". 😍 He showed off zkLib, which ties executable implementations of proof systems directly to security proofs.
https://www.youtube.com/live/L_uz5rH50Sw

🔹 James Parker from Galois introduced zkLean - a DSL for specifying ZK statements in Lean. Definitely worth checking out if you're interested in this space!
https://www.youtube.com/live/O_bT89JK6_c

🔹 Jonathan Rouach from QEDIT discussed the motivation behind the development of a Lean end-to-end proof of the PLONK verifier.
https://www.youtube.com/live/dNLa5B2ER74