Saved in:
| Main Authors: | , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2512.07087 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912766850236416 |
|---|---|
| author | Bolan, Matthew Breitner, Joachim Brox, Jose Carlini, Nicholas Carneiro, Mario van Doorn, Floris Dvorak, Martin Goens, Andrés Hill, Aaron Husum, Harald Mejia, Hernán Ibarra Kocsis, Zoltan A. Floch, Bruno Le Bar-on, Amir Livne Luccioli, Lorenzo McNeil, Douglas Meiburg, Alex Monticone, Pietro Nielsen, Pace P. Osazuwa, Emmanuel Osalotioman Paolini, Giovanni Petracci, Marco Reinke, Bernhard Renshaw, David Rossel, Marcus Roux, Cody Scanvic, Jérémy Srinivas, Shreyas Tadipatri, Anand Rao Tao, Terence Tsyrklevich, Vlad Vaquerizo-Villar, Fernando Weber, Daniel Zheng, Fan |
| author_facet | Bolan, Matthew Breitner, Joachim Brox, Jose Carlini, Nicholas Carneiro, Mario van Doorn, Floris Dvorak, Martin Goens, Andrés Hill, Aaron Husum, Harald Mejia, Hernán Ibarra Kocsis, Zoltan A. Floch, Bruno Le Bar-on, Amir Livne Luccioli, Lorenzo McNeil, Douglas Meiburg, Alex Monticone, Pietro Nielsen, Pace P. Osazuwa, Emmanuel Osalotioman Paolini, Giovanni Petracci, Marco Reinke, Bernhard Renshaw, David Rossel, Marcus Roux, Cody Scanvic, Jérémy Srinivas, Shreyas Tadipatri, Anand Rao Tao, Terence Tsyrklevich, Vlad Vaquerizo-Villar, Fernando Weber, Daniel Zheng, Fan |
| contents | We report on the Equational Theories Project (ETP), an online collaborative pilot project to explore new ways to collaborate in mathematics with machine assistance. The project successfully determined all 22 028 942 edges of the implication graph between the 4694 simplest equational laws on magmas, by a combination of human-generated and automated proofs, all validated by the formal proof assistant language Lean. As a result of this project, several new constructions of magmas satisfying specific laws were discovered, and several auxiliary questions were also addressed, such as the effect of restricting attention to finite magmas. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_07087 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale Bolan, Matthew Breitner, Joachim Brox, Jose Carlini, Nicholas Carneiro, Mario van Doorn, Floris Dvorak, Martin Goens, Andrés Hill, Aaron Husum, Harald Mejia, Hernán Ibarra Kocsis, Zoltan A. Floch, Bruno Le Bar-on, Amir Livne Luccioli, Lorenzo McNeil, Douglas Meiburg, Alex Monticone, Pietro Nielsen, Pace P. Osazuwa, Emmanuel Osalotioman Paolini, Giovanni Petracci, Marco Reinke, Bernhard Renshaw, David Rossel, Marcus Roux, Cody Scanvic, Jérémy Srinivas, Shreyas Tadipatri, Anand Rao Tao, Terence Tsyrklevich, Vlad Vaquerizo-Villar, Fernando Weber, Daniel Zheng, Fan Rings and Algebras Logic in Computer Science We report on the Equational Theories Project (ETP), an online collaborative pilot project to explore new ways to collaborate in mathematics with machine assistance. The project successfully determined all 22 028 942 edges of the implication graph between the 4694 simplest equational laws on magmas, by a combination of human-generated and automated proofs, all validated by the formal proof assistant language Lean. As a result of this project, several new constructions of magmas satisfying specific laws were discovered, and several auxiliary questions were also addressed, such as the effect of restricting attention to finite magmas. |
| title | The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale |
| topic | Rings and Algebras Logic in Computer Science |
| url | https://arxiv.org/abs/2512.07087 |