News for hackers. Stuff that matters.
Re:The math is haunted by Tainnor on Thursday July 31, 2025 @07:34AM (#44744556)
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).

Re:The math is haunted by daxfohl on Thursday July 31, 2025 @04:55PM (#44750032)
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.
Re:The math is haunted by Tainnor on Thursday July 31, 2025 @04:59PM (#44750072)
Dually, sometimes you'll have something like 1 < 0 as an assumption, which means you can close any goal.