Hacker News Reader

Comment by cnity | Hacker News Reader

This highlights I think what is an ultimate pitfall of something like Lean. It is something like this: when an assumption is broken or violated in mathematics, the whole field of mathematics can _grow_. Non-euclidean geometry, imaginary numbers, etc are all examples of this. Trying to cram maths into a programming language sounds like it would constrain it, removing the creativity and reducing all maths to a search space.

View on HN

Lean does not reduce the mathematical search space as you suggest. Yes there is a fixed, compact low-level logical core that everything above it depends on. But this is equivalent to an encoding of the logical foundations that mathematics, that formal mathematics depends on in any case. On top that you have mathematical theories built on assumptions (axioms) and you can specify whatever axioms you like and change them at will. To use your analogy: the "search space" is parameterised by user-defined sets of axioms and assumptions.

Could one possibly use Lean to make up their own mathematical model that is wrong but mostly holds up for a while? Kind of like a Sudoku where it’s all working and then you realize one thing doesn’t work so the rest has to be torn down.

I have young kids, and in exploring why boats float I suggested the four elements model. They tested it with bottles full of air and water and earth and it all kind of held up until they found a bowl that floats. Making a wrong model helped the learning process more than telling them the right model. I loved every minute of the science.

You can add any axiom you want in Lean and then see what follows (although what follows might be that you prove a contradiction). See the article for details.

I don't know if there's a way to remove axioms, nor do I think you can change the logical foundations (which are based in type theory).

And even aside from defining your own axioms, you can have the same experience just by taking the wrong path in a proof. You'll frequently try something and the goal checker will say that the only thing left is to prove 1 < 0 or such. That's obviously impossible, but it doesn't mean the theorem you're trying to prove is wrong, it just means that you've painted yourself into a corner with your proof attempt, and need to back up and try something else.

Dually, sometimes you'll have something like 1 < 0 as an assumption, which means you can close any goal.

One view of this article is that it is about doing exactly that, building an intentionally broken axiom and playing with it until it breaks down. (Shows an example "math_is_haunted" axiom that "proves" 2 + 2 = 6 and then also the contradictory state that 2 + 2 != 6.)

Reply on news.ycombinator.com