News for hackers. Stuff that matters.
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.