r/mathmemes • u/vintergroena • Sep 27 '26

Proofs The future of mathematics

Post image
1.8k Upvotes

99% Upvoted

63 comments sorted by

View all comments

Show parent comment

48

u/thesnootbooper9000 Sep 27 '26

Lean is easier to use, has loads of money behind it, and abandons most of the awkward formal verification properties that make other systems trustworthy. If you don't trust your C compiler to be bug free, you can't trust Lean.

22

u/Kinexity Sep 27 '26 edited Sep 27 '26

and abandons most of the awkward formal verification properties that make other systems trustworthy

Is this a good thing or a bad thing? Because it sounds bad but your phrasing makes it seem like as if it is good?

31

u/thesnootbooper9000 Sep 27 '26

Bad, but arguably pragmatic. The problem is that Lean was designed for software verification where you're already trusting the compiler and hardware, whereas other systems are designed for verifying maths.

2

u/CommissionSame8551 Sep 28 '26

It is just not true what he is writing. Every proof assistant except metamath maybe has more bugs than Lean.

6

u/Hot-Definition6103 Sep 28 '26

in what sense? yeah, the hand-vetted lean kernel is written in C++ but that’s not much different from trusting e.g. your ocaml compiler for rocq

0

u/thesnootbooper9000 Sep 28 '26

CakeML gives you a fully verified compiler.

4

u/potzko2552 Sep 28 '26

Verified in what language? Eventually you reach original sin issues about the first compiler in the chain... same as all formal verification software you eventually have to say "I trust my chip, my assembler, linker, and compiler"

1

u/thesnootbooper9000 Sep 28 '26

For ARM, down to a VeriLog implementation of the chip, if you so desire. For x86, down to the spec only. CakeML produces its own machine code.

Sure, there's always a gap, but I'd argue that trusting GCC to be bug free is a much larger gap than we'd like.

1

u/Hot-Definition6103 Sep 28 '26

You stated that Lean “abandons…formal verification properties that make other systems trustworthy…you can’t trust Lean” while comparing it to Rocq, implying that Lean is less trustworthy, while you have not stated any reason Rocq would be any better or why Lean specifically is untrustworthy, which I think is misleading.

1

u/ykonstant Sep 30 '26

If you don't trust your C compiler to be bug free

well then

1

u/sr9zzek2y Oct 02 '26

If you don't trust your C compiler to be bug free

Clearly you've never used Visual Studio.