logoalt Hacker News

mrtesthahlast Saturday at 2:17 AM1 replyview on HN

They probably need to be able to read and understand the lean language.


Replies

aidenn0last Saturday at 4:29 AM

I can read and understand e.g. Python, but I have seen subtle bugs that were hard to spot in code generated by AI. At least the last time I tried coding agents (mid 2025), it was often easier to write the code myself then play "spot the bug" with whatever was generated. I don't know anything about Lean, so I was wondering if there were similar pitfalls here.

show 4 replies