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 .
{"deleted":true,"id":50218910,"parent":50215079,"time":1792825450,"type":"comment"}