Adolfo Neto1d ago
The Proof in the Code: How a Truth Machine Is Transforming Math and AI (English Edition)
Kevin Hartnett

R$ 103,56

 It’s still too expensive for me. I’ll wait until it goes down to about 50 reais in a sale.

link.amazon/B0bTKD9mc

#LeanLang #LeanProver

The Proof in the Code: How a T...
The Proof in the Code: How a Truth Machine Is Transforming Math and AI (English Edition) - eBooks em Inglês na Amazon.com.br

Compre The Proof in the Code: How a Truth Machine Is Transforming Math and AI (English Edition) de Hartnett, Kevin na Amazon.com.br. Confira também os eBooks mais vendidos, lançamentos e livros digitais exclusivos.

Adolfo Neto1d ago
Silvio Meira (a legend in Brazilian computer science) shared this image and this link

How Terry Tao Became an Evangelist for AI in Math

#LeanLang

www.quantamagazine.org/how-terry-ta...
Joachim Breitner5d ago

Does

> This way, you can achieve a spectacular 200x speed-down on your code with the added bonus of far fewer supported operations and an overall suboptimal experience.

make you curious, then read https://juliahimmel.de/blog/float-qanda/

(If you don't read that text, rest assured that that quote is taken out of context and Julia is not making your programs slower.)

#leanlang #floatingpoint

Floats in Lean 4.33

Here is a little informal Q&A-style post about the changes to Float in Lean 4.33. The questions are meant to be read from top to bottom, not in arbitrary order. This is not an “official” communication by the Lean FRO, whatever that may mean.

Julia Markus Himmel
LeanJun 18

Lean 4.31.0 is released.

This consolidation-heavy release brings 305 changes. For those working on verified software: repeat/while loops are now verifiable without requiring source changes, expanding through whileM to support a one-step unfolding lemma. The new experimental mvcgen' tactic, reimplemented from the ground up on the SymM-based symbolic evaluation framework, can outperform mvcgen by a factor of over 100x on some synthetic benchmarks.

Library authors and package maintainers also gain a built-in linting framework through lake lint, with linters upstreamed from Batteries and Mathlib.

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

#LeanLang #LeanProver #ProofAssistant #FormalVerification

Adolfo NetoJun 16
#LeanLang 0.1 was released 12 years ago today! The creator of Lean is Brazilian. His name is Leonardo de Moura. xcancel.com/leanprover/s...
Adolfo NetoJun 12
The Proof in the Code: How a Truth Machine Is Transforming Math and AI
by Kevin Hartnett
#LeanLang #Lean4 #LeanProver
https://amzn.to/4xnAIj8
Amazon.com

Adolfo NetoJun 12
The Proof in the Code: How a Truth Machine Is Transforming Math and AI by Kevin Hartnett #LeanLang #Lean4 #LeanProver amzn.to/4xnAIj8

The Proof in the Code: How a T...
The Proof in the Code: How a Truth Machine Is Transforming Math and AI: Hartnett, Kevin: 9780374620059: Amazon.com: Books

The Proof in the Code: How a Truth Machine Is Transforming Math and AI [Hartnett, Kevin] on Amazon.com. *FREE* shipping on qualifying offers. The Proof in the Code: How a Truth Machine Is Transforming Math and AI

Adolfo NetoJun 12
Leonardo de Moura, Kevin Jartnett, Jeremy Avigad and Sebastian Ullrich Panel Series: The Proof in the Code - The Builders #LeanLang #lean4 #LeanProver
Adolfo NetoJun 11
#LeanLang
Adolfo NetoJun 10
"𝐓𝐡𝐞 𝐏𝐫𝐨𝐨𝐟 𝐢𝐧 𝐭𝐡𝐞 𝐂𝐨𝐝𝐞 is out, Kevin Hartnett's new book on the development of Lean and Mathlib. It tells the story of how Lean grew from a code-checking program into a tool now used across mathematics and " improv comedy groups #LeanLang

The Proof in the Code - Quanta...
The Proof in the Code - Quanta Books

The inside story of Lean, a computer program that answers the age-old question: How do you know if something is true?

Quanta Books