by @adolfoneto.elixiremfoco.com
Posts about Lean, an open-source functional programming language and interactive theorem prover: https://lean-lang.org/
zii This packing of 15 equal disks in a circle was conjectured to be optimal by U. Pirl in 1969. I've developed a computer-assisted proof of its optimality, and I'm currently formalizing it in Lean. Independent verification and feedback are welcome! github.com/ziifave/uneq... #MathSky #Lean4
Adolfo Neto Well, well. #LeanLang "Leo the first proof assistant dev to be invited to the white house???? damn plbros we're really moving up in life huh? makes me tear up a lil" @kirancodes.me posted on X
FAUN.dev MathCode takes a math problem in plain words and tries to prove it in Lean 4. Subscribe to AILinks at faun.dev/newsletter