Are Pro chatbots noticeably better for Lean?

Stream: new members

[Timothy Chow]

I'm considering shelling out some money for a premium / Pro version of one of the well-known models (Gemini, ChatGPT, etc.), but before doing so, I'd like to get a sense of whether they are likely to give me noticeably superior performance when it comes to Lean questions. (I'm also interested in their general mathematics capabilities, but I recognize that that's getting off-topic for this forum.) Is there any evidence, even anecdotal evidence, that the pay versions are significantly more "knowledgeable" about Lean? If so, are any of them particularly good, or are they all about the same?

[Snir Broshi]

for questions rather than writing proofs, I recommend trying this free AI: https://deepwiki.com/leanprover-community/mathlib4/. It has access to the entire Mathlib repo, and it's great at finding stuff, e.g. "group cosets", "indicator function on a set", "convex function has a unique minimum". I think it'll beat any chatbot in Lean knowledge when using it in the browser, not sure how it compares to other tools that have access to a codebase (e.g. Claude Code / Codex)

[Snir Broshi]

Also it seems Aristotle is the current SOTA at writing proofs: #announce > Sign Up for the Aristotle API!

[Timothy Chow]

I tried signing up for Aristotle a couple of days ago but have not received any email. How long can I expect to wait? Or maybe access is limited?

[David Kinkead]

Sounds like we both signed up for Aristotle around the same time. I'm still waiting too. For what it's worth, I've found the pro version of Gemini to be significantly better than the standard versions of Gemini / ChatGPT / Perplexity when working with Lean. Gemini Pro is still not brilliant, but I find it helpful more often than not, which wasn't the case with the standard versions. You should be able to get a free trial for at least a month if you want to test it out first.

[Junyan Xu]

You should get several free Gemini Pro queries (3~5?) every day even without paying or signing up for a trial.
image.png
If you want Deep Think that does require an Ultra subscription ...