Frans #Faase’s blog, discussing Modbus, the new #Lean #math proof of Fermat’s Last Theorem, laser-cutting puzzle pieces, etc.
on 02026-09-08The Natural Number Game #tutorial for #Lean 4, starting with rfl and rw [assumptionname]. #toread
#Tutorial #documentation directory for #Lean 4, starting with the Natural Number Game. #toread
on 02026-06-14#Lean online playground storing the code in an URL fragment. This is supposed to be a solver for a couple of linear inequalities. But it takes forever to load and then I can’t figure out how to actually run anything.
on 02026-06-14The #Lean homepage uses “L∃∀N” as the logo but says, “Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code”. #formal-methods
on 02026-06-14You can install #LEAN in a subdirectory with more space by pointing the ELAN_HOME environment variable to it before running elan toolchain install stable or whatever. #documentation #formal-methods
“Dispatches from the possibly last days of human relevance” on Erdos’s Unit Distance Problem and how “a system called AlphaProof Nexus to settle nine more (!) Erdös problems, many of them in additive combinatorics, along with miscellaneous other open #math problems. Notably, in this case the AI also fully formalized its proofs in #Lean.” #AI #Scott-Aaronson
on 02026-06-01#HN discussion of the #AI #LEAN proof of Erdos problem 728, discussing AI and #formal-methods more generally, including the “Lean-language statement of the problem”, which is eight lines of code.
on 02026-01-16Terry Tao on #Mastodon explaining that #AI solved Erdos problem 728. “Interestingly, the proof contained some minor errors in it, but the AI tool Aristotle was able to automatically repair these gaps and produce a Lean-verified proof.” #math #LEAN
on 02026-01-16Kevin Buzzard’s #LEAN blog for the "Xena Project" to formalize mathematics in L∃∀N #logic, starting to take up #AI
on 02025-11-05#Harmonic is hiring part-time #LEAN 4 experts. #AI #logic
on 02025-11-05#video on Terence Tao talking about using #neural-networks in science and mathematics. “In particular, in situations where the #AI output can be independently verified, there are many promising applications, both in the sciences and in mathematics.” In particular, proof assistants. XTX sponsored both his talk and an AI math competition. He’s using #LEAN. Mostly he’s talking about collaborating in larger groups of humans using LEAN and other proof assistants, though, not the actual AI stuff.
on 02024-08-14notes on #formal-methods alternatives for #foundations-of-mathematics, covering #Xena, #Kevin-Buzzard, #LEAN, and #Metamath
on 02021-01-15