LeanCopilot and other imports

Stream: PrimeNumberTheorem+

[Terence Tao]

We have a pull request https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/438 (from my colleague at UCLA) using LeanCopilot. The Lean portion of the PR I can upload separately without Copilot, but I was wondering if there was any downside with modifying the lakefile of the main repository to incorporate tools such as Copilot. Would this require everyone else on the project to also install this import? I remember about a year ago we decided to not have any imports (e.g., Duper or Canonical) for the Equational Theories Project due to various technical issues, but I don't know how much of an issue these are nowadays.

[Alex Kontorovich]

Thanks Terry. I'm at the JMM now -- the Math Corps won an AMS award -- so will have limited access for a few days; but just wanted to chime in that I think I'd like to discourage use of outside tools, if possible. Once they're in the lakefile, now everyone is required to download them, even if they want to work on unrelated parts of the repo, right? Maybe for one or two tools it's not such a big deal, but it seems like it can snowball as more such tools come online? Can't these tools return a tactics-only solution (like show_term), that is, using built-in Mathlib tactics, so they don't need to be run every time? (Isn't this how AlphaProof/Harmonic/Logical Intelligence/etc work? If they solve a sorry, they return the Lean code and then you don't need to call their API again...) Does LeanCopilot not have that feature?

[Ruben Van de Velde]

I assume we'd commit the output of any llm, yeah, but adding it to the lakefile would automatically make the import available to use it