Comment by rafaelRiv

I do a lot of software dev with idris2 in my free time and this is the problem. Everytime I try llms with formal verification, llms tend to try to remove all type check and cheat. That is why I am soooo sceptical of people using lean will llm too .