IS there a way to get all the available theorems in Lean3?

Stream: new members

[venom Yu]

Hi, everyone! I want to design an Automated Theorem Prove agent with search method first. I wonder is there a way to get all the available theorems in Lean3? Since I need all the possible transitions. Thanks!!!

[Patrick Massot]

It isn't clear at all in what format you would need to get those theorem for your purposes. You should be aware that you are not the only one to have this idea. We even have a dedicated stream at https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving where you'll find many pointers to the already large academic literature on this topic.