Theorem 6. The following are equivalent: The binary expansion of 7.Here it's building a list with one element and saying all elements of this list are equivalent. So the following elements of the list are all equivalent to each other (there is a single element in the list)
It sounds like subtraction over Nats needs to be split into `sub?`, and `sub!`, the former returning an option, and the latter crashing, on underflow, as is the Lean convention?
To use the default `sub`, you should need to provide a witness that the minuend is >= the subtrahend...
The version with silent underflow is still useful, it should just be called `saturatingSub`, or something, so that mathematicians using it know what they're getting themselves into...
Now, of course, if you're careful with the definitions you use, there is no problem. But in the (increasingly relevant) context of automatic theorem proving with LLMs, this seems to defeat the 'groundtruthness' of Lean!
How do you make sure that the LLM doesn't reward hack a proof using these workarounds?
andyjohnson0•1h ago
[1] https://www.cantorsparadise.com/what-are-junk-theorems-29868...
akoboldfrying•8m ago