Weekly
News about Lean, the theorem prover and programming language.
Papers, talks, courses, events, funding, and press. 53 items, newest first.
Alexandre Rademaker says the course is probably the first Lean course taught in Portugal and is an official World Logic Day 2026 event. It uses The Hitchhiker's Guide to Logical Verification and is partly supported by Atlas Computing via a Schmidt Sciences grant.
Checked against: LinkedIn post
In a LinkedIn post, Martin Ciupa recaps the conversation, in which Terence Tao calls automating formalization (turning ordinary math into proof-assistant-checked form) the near-term change, stresses formal verification over trusting AI blindly, and highlights Lean-style autocomplete that fills a line or two at a time.
Checked against: LinkedIn post
Lean Together is an annual meeting for users, developers, and fans of the Lean programming language and theorem prover, covering formalized mathematics, software verification, infrastructure, and outreach. The meeting is open to everyone without cost, and talks will be recorded with speakers' permission and posted to the leanprover community YouTube channel.
Checked against: leanprover-community.github.io
The Lean Together 2026 schedule includes a mix of casual and more formal presentations, with talks running around four hours each day and staggered start times for different time zones. Recordings of all talks are on the Lean community YouTube channel.
Checked against: leanprover-community.github.io
Math, Inc. posted a full conversation in which Fields medalist Terry Tao sits down with Math Inc's @jessemhan and @jdlichtman to discuss the future of mathematics. Terry Tao says this style of writing proofs shows the inputs and outputs of a proof more clearly and predicts that "the definition of a mathematician will broaden."
Checked against: @mathematics_inc on X