Zulip Chat Archive

Stream: Equational

Topic: Citations to the ETP

Jose Brox (Dec 08 2025 at 11:01):

Are you aware of any citations to the ETP? (I know some, but probably not all of them). Can you share them here?

Jose Brox (Dec 08 2025 at 11:01):

@Shreyas Srinivas you have mentioned a citation at ICLR, can you share it?

Bruno Le Floch (Dec 08 2025 at 11:19):

There is Mikoláš Janota's paper which we cite, https://arxiv.org/abs/2508.15856 «Experimental Results for Vampire on the Equational Theories Project», exploring what proportion of the graph can be automatically proven by Vampire.

Shreyas Srinivas (Dec 08 2025 at 11:46):

https://arxiv.org/pdf/2504.10101

Bruno Le Floch (Dec 08 2025 at 11:46):

Papers, talks, and popularization by others

Talks/audio by us:

Shreyas Srinivas (Dec 08 2025 at 11:46):

Cody Roux is an author, so maybe that doesn't count

Bruno Le Floch (Dec 08 2025 at 11:48):

Yes, the second half of my message was by coauthors. I've added a line to clarify that.

Shreyas Srinivas (Dec 08 2025 at 11:49):

Is Mario's talk available online?

Bruno Le Floch (Dec 08 2025 at 12:01):

We are cited in the "Brief History" of Lean described by the Lean Focused Research Organization https://lean-lang.org/fro/about/

Bruno Le Floch (Dec 08 2025 at 12:03):

Some mathoverflow questions:
https://mathoverflow.net/questions/450890/is-there-an-identity-between-the-commutative-identity-and-the-constant-identity
https://math.stackexchange.com/questions/5093482/what-are-the-coatoms-of-the-partial-order-of-equations-in-the-signature-of-magma

Shreyas Srinivas (Dec 08 2025 at 14:09):

Bruno Le Floch said:

Papers, talks, and popularization by others

Here they say "A major advantage of this approach is that the collaboration is “trustless” – meaning no central trusted authority is required to verify the validity of contributions". This is not exactly true and I wrote 5 pages to make the case to be careful :smiling_face_with_tear:

Shreyas Srinivas (Dec 08 2025 at 14:21):

if there's one big takeaway from this project it is this : "Appoint many maintainers who understand the math, lean, and at least some parts of the tooling, and importantly those who can review the work."

Shreyas Srinivas (Dec 08 2025 at 14:22):

also even if we ignore all the complications, we have a central trusted authority, the lean kernel and the software stack that is runs on in the CI.

Shreyas Srinivas (Dec 08 2025 at 14:23):

We were essentially able to map-reduce this project and map-reduce requires centralised coordinators

Shreyas Srinivas (Dec 08 2025 at 14:35):

Also to correct a small point in @Marco Petracci 's thesis credits the project managment ticketing idea should be credited to both me and Pietro. Pietro implemented the CI scripts, but I came up with the idea, the dashboard, the initial automation, and the precise specs of the CI scripts on the Zulip and in contibutions.md . The state machine that's in the paper basically was mine. I set up the preliminary automation that didn't require explicit CI yaml scripting. Pietro then took on the CI writing tasks for moving tasks across labels (this was quite instructive for me in learning this CI scripting language melange of yaml and bash). Then we both managed and refined the process over two months of firefighting in PRs, including a lot of late night fixes.

Shreyas Srinivas (Dec 08 2025 at 14:43):

Pietro ofc should get full credit for fluently creating and managing most of the CI. Without that, this project would not have functioned at all.

Bruno Le Floch (Dec 08 2025 at 21:30):

There is also Judah Towery's Bachelor thesis.

Matthew Bolan (Dec 09 2025 at 18:57):

There are some citations on the OEIS at https://oeis.org/A103293 and https://oeis.org/A376640

Jose Brox (Dec 09 2025 at 22:41):

Matthew Bolan ha dicho:

There are some citations on the OEIS at https://oeis.org/A103293 and https://oeis.org/A376640

Those are cool, but I think for me no one will ever beat this one:
https://en.wikipedia.org/wiki/Axiomatic_system#Timeline_of_postulational_analysis

Shreyas Srinivas (Dec 09 2025 at 22:48):

We are also cited in the central groupoid Wikipedia article.

Shreyas Srinivas (Dec 09 2025 at 22:48):

But the author list there is incomplete

Jose Brox (Dec 09 2025 at 22:49):

I share the citations I had found too (some have already appeared above):

1.       The bbchallenge Collaboration. Determination of the fifth Busy Beaver value. Draft 2025 [cites the paper]. https://doi.org/10.48550/arXiv.2509.12337
2.      Janota. Experimental results for Vampire on the Equational Theories Project. Preprint 2025. https://doi.org/10.48550/arXiv.2508.15856
3.       Yoo. The Axiom-Based Atlas: A Structural Mapping of Theorems via Foundational Proof Vectors. Preprint 2025 [cites Tao’s blog]. https://doi.org/10.48550/arXiv.2504.00063
4.      Yang et al. FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory. Preprint 2025 [cites the project]. https://doi.org/10.48550/arXiv.2510.02335
5.      Dai, Song, Jiang, Wang. From data to Physics: an agentic large language model solves a competitive adsorption puzzle. Angewandte Chemie, 2025. https://doi.org/10.1002/ange.202512151
6. [NOT COMPLETELY SURE ABOUT THIS ONE, SINCE I CANNOT READ IT TO CONFIRM]. Dean, Naibo. On open questions, artificial intelligence, and mathematical difficulty: A précis. Mitteilungen der Deutschen Mathematiker-Vereinigung 33(3) 2025. https://doi.org/10.1515/dmvm-2025-0054

  1. Towery. Proof assistants and type theory. Bachelor thesis. 2025. https://www.math.unm.edu/sites/default/files/images/Judah_Towery_Honors_Thesis_corrected.pdf
  2. Robinson, Lawrence. The human visual system can inspire new interaction paradigms for LLMs. ICLR 2025 Workshop on Bidirectional Human-AI Alignment (BiAlign 2025) [cites the paper]. https://arxiv.org/pdf/2504.10101
    9.         Alper. Embracing AI and Formalization: Experimenting with Tomorrow's Mathematical Tools. Bulletin of the AMS 2025. https://sites.math.washington.edu/~jarod/papers/embracingAI.pdf
    10.      Petracci. Collaboration and innovation in the Equational Theories Project: formalizing Mathematics with Lean 4. Master thesis. 2025. https://amslaurea.unibo.it/id/eprint/35220/1/TESI_MAGISTRALE_MARCO_PETRACCI-finale.pdf
    11.       Cepelewicz. Mathematical beauty, truth and proof in the age of AI. Quanta Magazine 2025. Long scientific magazine article. https://www.quantamagazine.org/mathematical-beauty-truth-and-proof-in-the-age-of-ai-20250430/
    12.         Delahaye. Plongée dans les magmas. Pour la Science 6 572 (2025). Long scientific magazine article. https://www.pourlascience.fr/sr/logique-calcul/plongee-dans-les-magmas-des-structures-mathematiques-simples-mais-fecondes-27730.php
    13.      Other: Cited in the Brief History of Lean, https://lean-lang.org/fro/about/. Also 2 new entries in the OEIS. Also 2 mentions in Wikipedia. Also a Isaac Newton Institute for Mathematical Sciences workshop related to this project: Big Proof: formalizing mathematics at scale. https://www.newton.ac.uk/event/bprw03/

Shreyas Srinivas (Dec 09 2025 at 23:06):

So we have a bunch of citations but they are scattered all over the place.

Shreyas Srinivas (Dec 09 2025 at 23:07):

Some cite the paper draft. Some cite the repository, and some cite the blog posts.

Last updated: Dec 20 2025 at 21:32 UTC