What do you hope AI can help you achieve with Lean in 2025?

Stream: general

[Huajian Xin]

What do you hope AI can help you achieve with Lean in 2025? e.g. code completion, documentation, code refactoring, etc. These suggestions will provide valuable guidance to developers of AI systems for Lean. :smile:

[Frederick Pu]

Some sort ai based refactoring and metaproggraming capabilities. so that we can feed in a paper and get a bunch of preliminary definitions that can be distilled and refactored by us soup computers

[Kevin Buzzard]

Here's hoping for powerful translation of human mathematics into Lean. Not only will it help me get FLT done quicker, but it will help us to make much bigger math databases for AI to train on. Mathlib is in some sense an extremely high-quality dataset, we just need a lot more of it.

[Frederick Pu]

or using Lean for model based RL, so like train it on AIME questions for example but it needs to come up with it's formalisms from scratch with no underlying mathematics library. Would interesting to see if it's possible for it to implicitly come up with all the formalisms. That would prob be pretty far down the line since model based rl seems to be only for very small models (eg. n by n binary matrices) so far.

[Shreyas Srinivas]

Huajian Xin said:

What do you hope AI can help you achieve with Lean in 2025? e.g. code completion, documentation, code refactoring, etc. These suggestions will provide valuable guidance to developers of AI systems for Lean. :smile:

Translate coq and Isabelle tactic proof scripts to lean tactic proof scripts

[Shreyas Srinivas]

In a sense it is the dynamic algorithms version of LLM proof generation: given an existing proof for another proof system, can you adapt it to a lean proof.

[Shreyas Srinivas]

While this sounds like a challenge for old fashioned logical methods, the jumbled mess of tactic languages makes it a more diffuse challenge. So perhaps some modern AI "might" help.

[Frederick Pu]

related to the model-based RL a nice stepping-stone would be to have a bunch of valid and invalid proofs and the ai has guess the type signatures of all of the lemmas used in the proofs based on all of the tactic states

[Floris van Doorn]

Autoformalization of mathematical statements would be really nice, and hopefully more achievable than the autoformalization of proofs. It would be nice if I give it some LaTeX of a theorem + proof, and I've already formalized the definitions in them, and it would spit out (say) a theorem + a sequence of have statements for the claims in the proof, all of them sorried.

[Niels Voss]

I'm not sure if this is something that AI would be good at, but I would be interested in an AI that, upon entering a theorem statement, can identify structurally similar theorem statements in Mathlib, and upon completing a proof, can identify similarly structured proofs. For example, if you entered a proof for the isomorphism theorems for modules, it might identify the isomorphism theorems for groups as having similar structure. The main uses of this would be to speed up proofs by copying existing proofs from Mathlib, and potentially identifying new abstractions.

[Junyan Xu]

Request: train a model from benchmark data to predict the change in compile time of each file from the diff. If it works well, it would save time from experiments like those I'm doing at #20140.

[Junyan Xu]

Refactoring projects:

This is one of the large-scale mathlib refactoring projects that I'd like AI to help experiment with and accomplish if favorable.

Some smaller-scale refactoring projects that have been discussed a lot on Zulip include:

1. make docs#Finsupp and Polynomial operations computable, by making Finsupp a special case of DFinsupp.
2. make docs#AddMonoidAlgebra k G a structure with a single field G →₀ k, and make docs#Polynomial R reducibly defeq to AddMonoidAlgebra R ℕ.

It's probably feasible that the human just changes a few definitions, then ask an AI agent to fix any CI errors without changing the type of or deleting any declarations.

[Leni Aniva]

I hope I can train smaller AI models that can prove theorems like one of the LLMs with a billion parameters

[Jason Rute]

@Leni Aniva What if it was a smaller model that used the same amount of test-time compute. There is a lot of recent work suggesting that may be possible.

[Tyler Josephson ⚛️]

Make it much easier to convert scientific computing software from imperative code into Lean code, and autoformalize theorems about them!

[Huajian Xin]

Very good idea! Is the translation between Lean4 and Mathematica still maintained? There has been A Bi-Directional Extensible Interface Between Lean and Mathematica for Lean 2.

[Jason Rute]

I don’t really do day-to-day Lean formalization, but from listening to the community I think I’ve identified the following needs:

[Jason Rute]

There are many large Lean projects like FLT and PrimeNumberTheoremAnd. They proceed via a workflow using blueprints which are detailed hyperlinked LaTeX outlines of the proof, with dependency graphs and references to the Lean code as it’s being written. The user slowly fills in Lean code for each lemma in the Blueprint. It is a great visual display of progress and a place where AI could certainly help. The most ambitious help would be to have AI convert the definitions and lemmas (and proofs?) into Lean code, completing the blueprint automatically (this is a form of practical automformalization which I think is the largest ask). But I think there are also other use-cases of AI in this process.

[Jason Rute]

Similarly, Lean projects take a long time and in the process there are a lot of stubbed lemmas with sorry in them. The ability to fill in sorrys in a background process (say as part of CI or via some server which makes automatic PRs to a repo) has been a much requested feature (#general > Tactic worth running my PC overnight?). The closest we have come to this is LeanAgent (see the discussion in #Machine Learning for Theorem Proving > LeanAgent). While I think LeanAgent was a bit oversold, it showed the vast potential of such a feature, even with a mediocre theorem prover. Just being able to look up a lemma in Mathlib which matches the sorry theorem, or better yet two lemmas which need to be combined non-trivially to complete the sorry proof, could be a huge help. And if one can actually make a good theorem prover which fills in difficult sorrys it could be a massive game changer! It would probably change the way people write their projects. They would leave a lot more sorrys in the code in the hope that the AI would complete them. But the discussion about LeanAgent also highlighted a bunch of other real-world challenges. What happens if it just proves a sorry using inconsistent stubbed lemmas, or because sorry theorems behave wierd logically (although this is particially fixed in the newest version of Lean)? While this is probably useful information, it could be a bit noisy to get silly PRs proving theorems with obviously inconsistent lemmas. Also, one needs a good way to have the agent adapt in real time to the new code base which filled with new definitions and theorems. (LeanAgent addresses this with continual learning, but there are many other approaches as I outline in #Machine Learning for Theorem Proving > Keep AI theorem provers up-to-date.)

[Jason Rute]

I think many Lean users just want a good assistant which can close goals for them. Two problems with the current AI assistants for Lean are that (1) they are hard to install and therefore almost no one tries them out, and (2) they aren’t very good. I think many who have used Isabelle feel very fondly of Isabelle’s SledgeHammer. And I think that is because both it is easy to install (or so I’ve heard) and it is decent at completing easy goals. I think AI is probably better now than Sledgehammer, but users haven’t seen that in real life. As for user experience, the most user friendly system would be a VS Code plugin calling out to a (free?/cheap?) API similar to Github Copilot, Continue, Cursor, etc, but with better Lean integration. (Of course, APIs bring privacy concerns and are not for everyone, but that paradigm is taking off.) Another system design which also isn’t that bad are tactics which do one of three things: (1) suggest a next step, (2) complete a proof, or (3) suggest lemmas and definitions to use in the proof. (Lean Copilot has this interface for example, and Lean has a nice “Try this” feature to make it easy to accept the proof or suggestion from a tactic.) They could be hosted locally or use an API. I think there is still a lot of design room for small, fast locally hosted provers (not necessarily using transformers).

[Jason Rute]

The big challenge with developing these systems is a lack of good AI-Lean integration. For people on the ML side, metaprogramming in Lean is a huge challenge and most end up doing hacky ineffecient things like just writing a new file with AI-generated Lean code and running Lean on it. This works for benchmarks like MiniF2F (and maybe for the sorry-filling agent idea above), but it doesn’t work for in-the-editor Lean integration. On the Lean side, most Lean users don’t have experience hooking up tools to Lean. One needs better communication (both electonic communication between Lean and AI tools, and human communication between Lean experts and AI experts).

[Jason Rute]

I would like to see a lot more tools upstreamed to central Lean-maintained repos, which would make them usable to a variety of researchers and Lean tool designers. Some such tools which need to be upstreamed are the following:

• Tree search: Right now Aesop provides a drop in tree search tool which can easily be hooked up to any tactic suggestion tool. It is what Aesop and Lean Copilot use. I think it is a bit slow and clunky, but it is a good start. I think ABEL (#Machine Learning for Theorem Proving > ABEL) and if so, I’d love to see that upstreamed (@Fabian Glöckle). Having a common search tactic is better than every team/project redoing their own tree search.
• Data mining (especially data mining for locall or Githiub non-Mathlib projects so that you can have a custom model or a model with access to your code base)
• Lean/AI communication tools for tactics, plugins, and LLM tool-calling
• Premise/Lemma selection
• Ways to integrate AI with Lean’s environment. Lean has all sorts of internal discrimination trees for simp lemmas, rewrite lemmas, apply lemmas, or lemmas which can solve the current goal. It would be great to better incorporate and make usable such datastructures to modern AI systems. Imagine what one could do if the AI agent had much more information about what was actually available in the library.

[Jason Rute]

Also, in many ways the current AI tools are broken for silly reasons. ChatGPT would be a good Lean assistant for autoformalization, proofs, etc. if it understood Lean 4 vs. Lean 3. (I’ve heard Sonnet 3.5 is better.) There are good projects out there showing that one can automatically clean up a LLM generated proofs (Lyra, PALM, etc.) and auto-formalizations (LeanAide). Or that one can use an LLM to generate stubs for a different type of AI to fill in (Draft-Sketch-Prove, etc), or use the LLM recursively to clean up broken parts of the proof (Cobblestone, DeepSeek-Prover v1.5). It would be good to make such systems usable (and the repair components tools upstreamed so others can use them easily). Or even just generate more than one suggestion and test them all (DeepSeek-Prover v1). Honestly, many of these papers just use public APIs like GPT-3.5. I don’t see why we can’t quickly build these systems in practice right after such a paper comes out.

[Jason Rute]

Overall, we just need (1) to know what approaches and tools work in real life, not just on silly benchmarks, and (2) to build those in a way that people can use them. In many ways this shouldn’t be hard. We probably have lots of approaches that work, we just have never taken the time to verify that they work in real life and to make them available.

[Jason Rute]

Last, besides day-to-day tools, the three ultimate goals I see in this space are (1) large scale auto-formalization of real mathematics, and (2) large scale automatic verification of computer code, and (3) really powerful automated theorem proving. I certainly think we still need to be working toward those even if the research is messy, expensive, and not ready for users.

[Frederick Pu]

wasnt there a lean project where all the tree search is done in lean and u can just plug and play the model?

[Frederick Pu]

also i wonder how hard it would be to update Aesop to support rl, such as maintaining a policy and stuff. Cause doesn't Aesop already kind of do monte carlo tree search in some form?

[Jason Rute]

@Felix Weilacher I know of Aesop (which @Kaiyu Yang added the ability to use text for tactics which Lean parses, which is what Lean Copilot uses). Also, I don't know if Pantograph (@Leni Aniva) provides as similar tool? And there was Sagredo (@Kim Morrison).

[Jason Rute]

Aesop uses best-first search for which you can add your own scores (based on a value function), and ABEL (@Fabian Glöckle) uses MCTS and does RL.

[Frederick Pu]

what's ABLE

[Jason Rute]

A misspelling of #Machine Learning for Theorem Proving > ABEL.

[Frederick Pu]

is there a lean tactic for it or do they do hypertree search in leandojo

[Jason Rute]

it? I mentioned 5ish tools. Aesop is a tactic, and Lean Copilot has tactics (which use Aesop underneath). I don't know about the others.

[Frederick Pu]

i mean able

[Jason Rute]

Maybe ABEL (not "able", sorry) will be a tactic on top of Aesop when released:
Fabian Glöckle said:

Aesoprepl is not public yet (on it!), you'll need 200 lines on top of Aesop.

[Frederick Pu]

it would cool if Aesop had an api for making custom search modes, certainly would be cleaner (and hopefully run quicker) then trying to implment mcts or rmax search via lean dojo

[Leni Aniva]

Jason Rute said:

Felix Weilacher I know of Aesop (which Kaiyu Yang added the ability to use text for tactics which Lean parses, which is what Lean Copilot uses). Also, I don't know if Pantograph (Leni Aniva) provides as similar tool? And there was Sagredo (Kim Morrison).

What do you mean by using text for tactics? Like you can just execute rw [lemma_1, lemma_2] on a goal?

[Leni Aniva]

Jason Rute said:

Leni Aniva What if it was a smaller model that used the same amount of test-time compute. There is a lot of recent work suggesting that may be possible.

It may be, but I'm trying non language model based solutions

[Jason Rute]

Leni Aniva said:

Jason Rute said:

Felix Weilacher I know of Aesop (which Kaiyu Yang added the ability to use text for tactics which Lean parses, which is what Lean Copilot uses). Also, I don't know if Pantograph (Leni Aniva) provides as similar tool? And there was Sagredo (Kim Morrison).

What do you mean by using text for tactics? Like you can just execute rw [lemma_1, lemma_2] on a goal?

Yes, exactly! Look at this example: https://github.com/leanprover-community/aesop/blob/master/AesopTest/TacGen.lean
I also realize @Jannis Limperg added this feature and also worked on ABEL so he might have something to say.

[Jason Rute]

Leni Aniva said:

Jason Rute said:

Leni Aniva What if it was a smaller model that used the same amount of test-time compute. There is a lot of recent work suggesting that may be possible.

It may be, but I'm trying non language model based solutions

You should check out my Graph2Tac. I wish there was a Lean version. :( Also Tactician’s kNN (also benchmarked in that same paper).

[Martin Dvořák]

I have one wish that is about AI but without machine learning.
Is there any low-hanging fruit for what Aesop could do but doesn't because it would be too expensive?
Maybe we could have Aesop++ that is extremely slow but, when run overnight, might find proofs that Aesop fails to find.
@Jannis Limperg

[Jason Rute]

@Martin Dvořák what is the reason to what Aesop with no ML, but still something which runs for hours? Because it is easier/cheap to run on a laptop? Or because you have Aesop already and good ML tools seem so far away?

[Martin Dvořák]

Tbh, good ML tools no longer seem far away; AlphaProof dramatically changed my mind!
However, something like Aesop++ could possibly land right now.
Maybe there is low-hanging fruit that @Jannis Limperg could pick in just few hours of work.

[Jason Rute]

Also, one should really see what happens with Aesop when run for longer amounts of time. What you want to see is a log-linear plot similar to what we see in new AI papers on “test-time scaling”, but also we see in good AI for theorem proving projects. Here is the plot in the graph2tac paper. 7d140a2950b22b7b8b20e482a1d8fd375f96ec11.png Every ATP paper should have this plot and I am disappointed that most don’t. Any Aesop folks want to make it? Maybe you already have the data.

[Martin Dvořák]

As I pointed out at the beginning of this year
#general > Tactic worth running my PC overnight? @ 💬
I expect the results to be severely diminishing and I won't be disappointed if Aesop++ takes 10000x more time but solves only a little bit more than Aesop does.

[Jason Rute]

Again, such a plot should give you a feel for that without first having to run 10000x time. Or on the other hand, just try yourself. You can already change the timeout for Aesop.

[Martin Dvořák]

Yes but Aesop only tries to do some things and usually ends (successfully or not) without using up all allowed heartbeats.

[Jason Rute]

@Martin Dvořák have you tried running existing tools like LeanCopilot or LLMLean for longer periods?

[Martin Dvořák]

No. Do they do search the state space?

[Jason Rute]

Yes. Lean Dojo is just Aesop with machine learning picked tactics.

[Jason Rute]

I usually cite your post in circumstances like this, but it isn’t quite clear what more you need to be able do actual experiments with running such tools on projects for longer periods? What is stopping you from doing those experiments today? What would make it feasible for when a new tool (like ABEL) became available for you to instantly try it on real formalization projects?

[GasStationManager]

I am most interested in the reverse direction of the question. What can Lean help us achieve with AI? I believe Lean (and other interactive theorem provers) can and should be a big part of addressing two of the major challenges in (generative) AI today, hallucination and safety.

How to get there can be a bit of a chicken-and-egg problem. The current AI models are often not good at outputting correct Lean 4 syntax, nor at how best to use Lean, though that may be slowly changing. Here's hoping that as better tools (AI-based or otherwise) that helps humans are developed, they can also be used by AIs to become more proficient users of Lean.

[Leni Aniva]

Jason Rute said:

Leni Aniva said:

Jason Rute said:

Felix Weilacher I know of Aesop (which Kaiyu Yang added the ability to use text for tactics which Lean parses, which is what Lean Copilot uses). Also, I don't know if Pantograph (Leni Aniva) provides as similar tool? And there was Sagredo (Kim Morrison).

What do you mean by using text for tactics? Like you can just execute rw [lemma_1, lemma_2] on a goal?

Yes, exactly! Look at this example: https://github.com/leanprover-community/aesop/blob/master/AesopTest/TacGen.lean
I also realize Jannis Limperg added this feature and also worked on ABEL so he might have something to say.

Pantograph was able to execute tactics like this since the beginning

[Jason Rute]

@Leni Aniva I’m not exactly sure of your point. This feature (the ability to call the parser from inside the tactic monad) was first added to Lean 3 by Ed Ayers to support lean-gptf (the first neural theorem prover in Lean in thee PACT project). Also I assume @Jannis Limperg’s adjustments to Aesop came before Pantograph. But the point I’m trying to make is not who was first, or even which tool is better, but how can we get more ML/AI tools into the Lean FRO supported projects like Batteries, Qq, and Aesop (all projects which mathlib depends on). I think it is great that Lean Copilot and ABEL (?) use Aesop, because the Lean FRO supports Aesop (and most heavy mathlib users know how to use Aesop). And the fact that the Lean FRO doesn’t support Lean Copilot shows. It is often out of date and less well maintained, and not widely used. I don’t think it necessarily makes sense to have the Lean FRO support Lean Copilot or ABEL or LLMLean since their time is limited, but I would like to see them support integral reusable components to Lean, just like how they support the tree search in Aesop and Jannis’ extension to let you run tactics given as strings. If Pantograph is better, maybe it makes sense for small reusable parts of it to become supported by the Lean FRO. (I’d also love a side by side comparison of Pantograph’s search with Aesop’s search using the same tactic prediction model. I don’t think the current Aesop search is fast and I don’t like that it evaluates all tactic suggestion first, before moving down the search tree. Maybe these are fixed in ABEL’s modifications to Aesop.)

[Henrik Böving]

because the Lean FRO supports Aesop

@Jason Rute in what sense does the FRO support aesop?

[Leni Aniva]

Jason Rute said:

Leni Aniva I’m not exactly sure of your point. This feature (the ability to call the parser from inside the tactic monad) was first added to Lean 3 by Ed Ayers to support lean-gptf (the first neural theorem prover in Lean in thee PACT project). Also I assume Jannis Limperg’s adjustments to Aesop came before Pantograph. But the point I’m trying to make is not who was first, or even which tool is better, but how can we get more ML/AI tools into the Lean FRO supported projects like Batteries, Qq, and Aesop (all projects which mathlib depends on). I think it is great that Lean Copilot and ABEL (?) use Aesop, because the Lean FRO supports Aesop (and most heavy mathlib users know how to use Aesop). And the fact that the Lean FRO doesn’t support Lean Copilot shows. It is often out of date and less well maintained, and not widely used. I don’t think it necessarily makes sense to have the Lean FRO support Lean Copilot or ABEL or LLMLean since their time is limited, but I would like to see them support integral reusable components to Lean, just like how they support the tree search in Aesop and Jannis’ extension to let you run tactics given as strings. If Pantograph is better, maybe it makes sense for small reusable parts of it to become supported by the Lean FRO. (I’d also love a side by side comparison of Pantograph’s search with Aesop’s search using the same tactic prediction model. I don’t think the current Aesop search is fast and I don’t like that it evaluates all tactic suggestion first, before moving down the search tree. Maybe these are fixed in ABEL’s modifications to Aesop.)

What I mean is that Pg supports calling the parser inside the tactic monad

[Jason Rute]

@Henrik Böving Maybe I’m using the wrong organization. Is it more accurate to say “the mathlib maintainers” (some of whom are supported by the Lean FRO) at least keep Aesop up-to-date and working since it is a dependency of Mathlib?

[Jason Rute]

Or is that even wrong?

[Henrik Böving]

Kim (who is a full time FRO employee) makes a version bump to the transitive closure of mathlib dependencies, including aesop, when we release a version every month. The rest of the work on aesop is almost exclusively done by Janis from the LMU.

[Jason Rute]

@Henrik Böving That isn’t nothing. Lean Copilot for example doesn’t readily stay up-to-date with version bumps. (And I assume you run tests and make releases as part of this version bump?) But maybe it is also just a vibe check. Aesop seems more integrated into the Lean ecosystem and community, which is good. But you are right that I should leave the Lean FRO out of this.

[Frederick Pu]

is aesop integration limited to only RAG based models like lean copilote. Cause I noticed that in a lot of the deepseek prover generated they never use pattern matching when doing stuff like cases but instead do the weird cases with h (h) <;> thing. Is there any way to take a proof and split it into a sequence tactic state + next rule applications so that language models like deepseek can be pretrained on mathlib4 directly instead custom curated proofs?

[Jason Rute]

@Frederick Pu Aesop isn’t the tool parsing mathlib for data, but there are plenty of tools to do that at the tactic level (Lean Dojo, lean-training-data, and I assume pantograph). Also Lean Copilot (unlike ReProver) is not RAG based. It is just an LLM predictor with no RAG. The important thing for the current Aesop feature is that you have a model to suggest tactics as strings. I might be possible to use DeepSeek-Prover to suggest a whole proof (if you could run it conditioned on the goal state) and then wrap that proof in something like by to get it to behave as a single tactic. I don’t think you could do DeepSeek-Prover v1.5 style MCTS where you take a proof, find the errors and start repairing there. But since many papers do this, it would probably be a good feature to support (in some tool, not necessarily Aesop).

[Ilmārs Cīrulis]

For me it is search for theorems and definitions.

[Jason Rute]

@Lessness what do you feel that existing tools like https://www.moogle.ai and https://leansearch.net don’t offer? (Or are you talking about another type of search like local project search? Or lemma suggestions for the current goal?)

[Frederick Pu]

at least from personal experience they usually don't find what im looking for, and i end up searching manually on mathlib4 docs instead

[Henrik Böving]

You should at least be using loogle.lean-lang.org, mathlib4 docs search is strictly weaker than it

[Ruben Van de Velde]

Hmm, I've found the docs search nicer when I don't know a name exactly

[Ilmārs Cīrulis]

@Jason Rute I didn't know about leansearch.net, will probably try it out. Moogle.ai doesn't always find what I need.

Local project search would be, I believe, something nice, too. :thumbs_up: A generalization of existing search tools.

[Jason Rute]

I really don’t understand why the search in the docs is so bad. Why can’t they just use one of the others? They already have the Google Site Search button. (But I’ve been complaining about this for years now, so I don’t think it will change.)

[Jason Rute]

Do folks like loogle? I guess the challenge is that you have to learn a specific search grammar.

[Henrik Böving]

Jason Rute said:

I really don’t understand why the search in the docs is so bad. Why can’t they just use one of the others? They already have the Google Site Search button. (But I’ve been complaining about this for years now, so I don’t think it will change.)

the hosted documentation is a frontend online site that has no backend, the search mechanism itself is made not so clever on purpose so your browser can even deal with the volume of strings it has to search through every time you type.

Jason Rute said:

Do folks like loogle? I guess the challenge is that you have to learn a specific search grammar.

Yes, loogle is amazing, I've never felt the need to use any AI search tool to find a theorem so far.

[Jason Rute]

@Henrik Böving But there is already a search using google button. Why not ones for leansearch, Moogle, and loogle?

[Jason Rute]

Moogle for example has the same search syntax as google where the query is in the url.

[Henrik Böving]

The search for the google button is an artifact back from when doc-gen was only used for mathlib. Loogle etc. are hosted only for mathlib currently, there are projects that host documentation with doc-gen that do not have these hosted services. One could configure that through a config file for doc-gen or something it's just not something I've done yet. And as a side note, given the fact that neither leansearch nor moogle can even be set up to work with other projects currently I also don't really see why doc-gen should include them, for loogle i do see a potential point.

[Jason Rute]

Ok, thanks for the clarification. I still think the situation is not ideal, but at least I see some reasoning behind it.

[Jason Rute]

@Frederick Pu and @Lessness What are examples of what you can’t find in those tools? Is it because they are out of date, or because they don’t understand what you are looking for?

[Jason Rute]

(Moogle unfortunately has not been kept up-to-date last I checked.)

[Jason Rute]

@Jiang Jiedong do you think learn search for custom projects would ever be a thing? I guess I don’t know how it works and if that makes sense or is crazy. (Also is there any description of how it works anywhere?)

[Frederick Pu]

i think the issue is that i usually try to search for new fields that i dont understand. so ig my queries are too vague. for example the query ​conditional probability just returns a bunch of parser definitions.

[Jiang Jiedong]

Jason Rute said:

Jiang Jiedong do you think learn search for custom projects would ever be a thing? I guess I don’t know how it works and if that makes sense or is crazy. (Also is there any description of how it works anywhere?)

I believe this is a very good and achievable idea! Here is the paper of LeanSearch

The preparing process doesn’t involve training, only involves inference using some large embedding model.

[Notification Bot]

A message was moved here from #general > What do you hope AI can help you achieve with Lean in 2025? by Jason Rute.

[Notification Bot]

A message was moved from this topic to #general > Decomposing pattern matching tactics for AI by Jason Rute.

[Jason Rute]

Frederick Pu said:

i think the issue is that i usually try to search for new fields that i dont understand. so ig my queries are too vague. for example the query ​conditional probability just returns a bunch of parser definitions.

I tried this in Moogle: https://www.moogle.ai/search/raw?q=conditional%20probability IMHO, it is better than you suggested. The first two suggestions are indeed parser terms, but if you follow the links they are the notations for conditional probability:

scoped notation μ "[" s "|" t "]" => ProbabilityTheory.cond μ t s
scoped notation:60 μ "[|" t "]" => ProbabilityTheory.cond μ t

I think one of the large issues here is that notations are displayed poorly in Moogle (and in doc gen, as Moogle just uses the way they are displayed in doc gen). But I agree that docs#ProbabilityTheory.cond should appear higher and some of the other stuff on top is not related to conditional distribution. But again, docs#ProbabilityTheory.cond is still not that far down the list. Of course, we shouldn't be content with mediocre tools. One short-term solution is to click the :thumbs_up:/:thumbs_down: buttons as appropriate.

[Jason Rute]

(I wanted to try Lean Search too, but I'm getting a bad gateway error. And last I remember it didn't cover definitions, just theorems, but maybe that has changed. cc @Jiang Jiedong )

[Jiang Jiedong]

Jason Rute said:

(I wanted to try Lean Search too, but I'm getting a bad gateway error. And last I remember it didn't cover definitions, just theorems, but maybe that has changed. cc Jiang Jiedong )

The current version of LeanSearch supports searching definition. This is added in the last update.

[Jiang Jiedong]

I tried to search ‘conditional probability’ using LeanSearch, the definition docs#ProbabilityTheory.cond_apply is at 6th place and first 5 results are theorems related to this definition like
docs#ProbabilityTheory.cond_apply

[Jiang Jiedong]

If one uses query augmentation on query ‘conditional probability‘， the first 3 results are
docs#ProbabilityTheory.cond_apply
docs#ProbabilityTheory.cond_apply'
docs#ProbabilityTheory.cond

[Jiang Jiedong]

It is quite interesting to find out that LLM translate the first two theorems as “Conditional Probability Axiomatic Definition”. The definition property is 'more definitional' than the Lean definition.

[Eric Wieser]

I wonder if sorting results topologically would help here (with X < Y meaning that type_of% Y refers to X