News for hackers. Stuff that matters.
Re:"Why not just use Lean?" by seanhunter on Monday April 27, 2026 @03:02PM (#47925796)
Thank you for the correction I actually didn't realise that so have learned something.

Specifically for people who are interested it seems you have to replace the parallel postulate with a postulate that says every point is a saddle point (which is like the centre point of a pringle if you know what that looks like).

https://en.wikipedia.org/wiki/Pringles

Re:"Why not just use Lean?" by lmm on Monday April 27, 2026 @09:08PM (#47929336)
You can also replace it with a different postulate and get projective geometry, IIRC.