3 ms·

If you have a denominator composed of “n - k - 1”, I hardly find it surprising that if n=3 and k=2 that you have a slight problem… Anyway, check out Idris[2],

If you have a denominator composed of “n - k - 1”, I hardly find it surprising that if n=3 and k=2 that you have a slight problem… Anyway, check out Idris[2], it’s cool for this sort of thing

SmartestUnknown 3y ago
Exactly lol. Not sure why everyone is taking the contribution of lean in finding the error so seriously. I would be more impressed when some mathematician finds a more severe error in their proofs with the help of theorem provers (meaning a mistake in their own intuition).