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.

▲

WorldMaker 10 days ago | parent | next [-]

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.)

▲

Tainnor 10 days ago | parent | prev [-]

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).

▲

daxfohl 10 days ago | parent [-]

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.

	▲	Tainnor 10 days ago \| parent [-]
		Dually, sometimes you'll have something like 1 < 0 as an assumption, which means you can close any goal.