Lean can check Lean code, not arbitrary code. There's no telling what gets lost in translation. There's other formal verification systems out there like Z3 which live alongside the code and can verify the actual implementation. There's so much hype around Lean but few people actually understand it. But hey who needs to understand anything anymore? We have vibe coding!

And whole article consists of blatantly Claude-generated text. Way to throw credibility out the window.

For the love of God please stop puking slop everywhere and write some copy by hand.

So many posts nowadays might as well just be the one-shot prompt and a one line summary.

For example, "I asked Claude to formally verify Python with Lean. It found lots of bugs. I checked a few by hand... just kidding!!"

Same approach for Julias stdlib: https://discourse.julialang.org/t/formalizing-julia-in-lean-...