Paper feed

Stream: Machine Learning for Theorem Proving

[fzyzcjy]

By the way, may I know the feed sources (feeds of AI math papers)? Thanks!

[Jason Rute]

I have a few sources. One is a Google scholar alert for machine learning "theorem proving". That is where I found this.

[fzyzcjy]

Thank you - I will add this now! Is it OK if I ask about the other sources?

[Kevin Buzzard]

ArXiv does daily mailshots (this is how I keep up with number theory, by following math.NT, although of course I see a lot of number theory which isn't my particular area of expertise this way)

[fzyzcjy]

Thank you! Then I will follow cs.AI/cs.LG as well.

[Jason Rute]

I’m making a new topic on feeds to find papers for Machine Learning for theorem proving.

[Jason Rute]

I’m on my phone, but it would be good to move some of the discussions from the other thread here.

[Jason Rute]

Besides my Google scholar alert, I also have an RSS feed for arXiv papers. I’m have trouble finding the link, but the query is

search_query=( "theorem proving" OR "theorem provers" OR "theorem prover" ) AND (neural OR transformers OR "machine learning" OR "deep learning" OR "language model" OR "artificial intelligence" OR AI)&id_list=&start=0&max_results=10

[Jason Rute]

And I look through the ICLR OpenReview papers for appropriate keywords.

[Jason Rute]

And the yearly meetings MATH-AI and AITP.

[Jason Rute]

And there are lots of twitters, mentioned in another thread here. (#Machine Learning for Theorem Proving > Other places discussing neural theorem proving ). Albert Jiang’s is one of the best.

[Jason Rute]

(Although Twitter/X is becoming more annoying. You have to be logged in to see tweet threads and the most recent posts.)

[Notification Bot]

A message was moved here from #Machine Learning for Theorem Proving > Paper: Enhancing Neural Theorem Proving through Data Augm... by Jason Rute.

[Notification Bot]

A message was moved here from #Machine Learning for Theorem Proving > Paper: Enhancing Neural Theorem Proving through Data Augm... by Jason Rute.

[Notification Bot]

A message was moved here from #Machine Learning for Theorem Proving > Paper: Enhancing Neural Theorem Proving through Data Augm... by Jason Rute.

[Notification Bot]

A message was moved here from #Machine Learning for Theorem Proving > Paper: Enhancing Neural Theorem Proving through Data Augm... by Jason Rute.

[Notification Bot]

A message was moved here from #Machine Learning for Theorem Proving > Paper: Enhancing Neural Theorem Proving through Data Augm... by Jason Rute.

[fzyzcjy]

Thank you so much! I will add all into my daily workflow :)

[Adam Topaz]

We have the following page on the community webpage: https://leanprover-community.github.io/papers.html

What do people think about adding a section for papers about machine learning and lean? It seems that there is sufficient interest!

[Alex Sanchez-Stern]

We'll probably eventually want a page somewhere with all machine learning and theorem proving papers, not just those in lean, since the techniques aren't generally lean-specific.

[Adam Topaz]

Sure, but it’s not clear whether that should go on the leanprover community webpage

[Jason Rute]

All papers is tricky because it’s hard to draw the line. I tried once to make a list, but it only goes up to last year.

[Jason Rute]

By draw the line I mean when is a paper just about ATP but not ML or about ML and math, but not (formal) theorem proving.

[Jason Rute]

Also, what to do about all the 2 page abstracts in AITP, sometimes the only place results are “published”?

[Alex Sanchez-Stern]

Ah sure, maybe "all" isn't the right distinction, but whatever qualifies a particular lean paper should probably also qualify a Coq or Isabelle paper. So, if a 2 page abstract at AITP in Coq doesn't qualiy, a 2 page abstract at AITP in Lean wouldn't either. I don't know if restricting to Lean really helps with the magnitude of papers either, most of the papers out of the ML community are in Lean anyway, and many of the Coq/Isabelle ones come from the PL community where papers tend to be fewer and less incremental.

[Alex Sanchez-Stern]

Adam Topaz said:

Sure, but it’s not clear whether that should go on the leanprover community webpage

Oh yeah, it might not make sense to put that list on the lean prover page. But if folks are looking for a list of papers on ai for theorem proving to track the different ideas and state-of-the-arts, they would probably want a list in another location that isn't prover-specific.