Hacker News Reader

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

View on HN

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.

Reply on news.ycombinator.com