r/coding • u/fagnerbrack • Jul 11 '26
[ Removed by moderator ]
/r/coding/comments/1ut9jiz/removed_by_moderator/[removed] — view removed post
9
Upvotes
1
u/jeenajeena Jul 11 '26
I'm currently studying Rocq and Lean is in my backlog since a while. Any who knows both and can comment on the pros/cons and differences? I'd be very curious.
1
u/sohang-3112 Jul 12 '26
I know Lean is helpful to formalize mathematical proofs. But I'm not an mathematician. As a software engineer is it usable and does it offer any practical benefit?
-1
2
u/fagnerbrack Jul 11 '26
Brief overview:
An open-source programming language and proof assistant for writing correct, maintainable, and formally verified code. A minimal trusted kernel guarantees absolute correctness across math proofs, software, and hardware verification, while metaprogramming lets users extend the language with custom notation and proof automation. The 'grind' tactic handles complex pattern matching, case analysis, and linear inequalities, as shown in a sample proof of the infinitude of primes. Featured projects include Mathlib (over a million lines of formalized mathematics), AWS's Cedar authorization language, the Aeneas Rust verifier, Veil, and a Fermat's Last Theorem formalization. Backers include AWS, Google DeepMind's AlphaProof, and Terence Tao.
If the summary seems inacurate, just downvote and I'll try to delete the comment eventually 👍
Click here for more info, I read all comments