My current model is that LLMs are better if you are working on some mainstream problem domain using a mainstream tech stack (language, library, etc.).
Yes, I have the same impression. Generating Java or Python code using popular libraries: mostly okay. Generating Lean code: does not compile even after several attempts to fix the code by feeding the compiler errors to LLM.
Yes, I have the same impression. Generating Java or Python code using popular libraries: mostly okay. Generating Lean code: does not compile even after several attempts to fix the code by feeding the compiler errors to LLM.