[pmarreck]

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]

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