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.
Re:The math is haunted
by WorldMaker on Thursday July 31, 2025 @05:43PM
(#44750535)
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.)
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.