[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1145/3636501.3636947acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article
Open access

Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit Conjecture

Published: 09 January 2024 Publication History

Abstract

We describe a formalization in Lean 4 of Giles Gardam's disproof of Kaplansky's Unit Conjecture. This makes use of a combination of deductive proving and formally verified computation, using the nature of Lean 4 as a programming language which is also a proof assistant.
Our goal in this work, besides formalization of the specific result, is to show what is possible with the current state of the art and illustrate how it can be achieved. Specifically we illustrate real time formalization of an important mathematical result and the seamless integration of proofs and computations in Lean 4.

References

[1]
Yves Bertot. 2008. A short presentation of Coq. In International Conference on Theorem Proving in Higher Order Logics. 12–16.
[2]
Thomas F Bloom. 2021. On a density conjecture about unit fractions. arXiv preprint arXiv:2112.03726.
[3]
Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of functional programming, 23, 5 (2013), 552–593.
[4]
Kenneth S Brown. 2012. Cohomology of groups. 87, Springer Science & Business Media.
[5]
Kevin Buzzard, Johan Commelin, and Patrick Massot. 2020. Formalising perfectoid spaces. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. 299–312.
[6]
Marcelo Campos, Simon Griffiths, Robert Morris, and Julian Sahasrabudhe. 2023. An exponential improvement for diagonal Ramsey. arxiv:2303.09521.
[7]
William Carter. 2014. New examples of torsion-free non-unique product groups. Journal of Group Theory, 17, 3 (2014), 445–464.
[8]
Sander R Dahmen, Johannes Hölzl, and Robert Y Lewis. 2019. Formalizing the solution to the cap set problem. arXiv preprint arXiv:1907.01449.
[9]
Nicolaas Govert De Bruijn. 1994. A survey of the project AUTOMATH. In Studies in Logic and the Foundations of Mathematics. 133, Elsevier, 141–161.
[10]
Giles Gardam. 2021. A counterexample to the unit conjecture for group rings. Annals of Mathematics, 194, 3 (2021), 967–979.
[11]
Georges Gonthier. 2008. Formal proof–the four-color theorem. Notices of the AMS, 55, 11 (2008), 1382–1393.
[12]
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, and Sidi Ould Biha. 2013. A machine-checked proof of the odd order theorem. In International conference on interactive theorem proving. 163–179.
[13]
Georges Gonthier and Assia Mahboubi. 2010. An introduction to small scale reflection in Coq. Journal of Formalized Reasoning, 3, 2 (2010), Jan., 95–152. https://doi.org/10.6092/issn.1972-5787/1979
[14]
W. T. Gowers, Ben Green, Freddie Manners, and Terence Tao. 2023. On a conjecture of Marton. arxiv:2311.05762.
[15]
Benjamin Grégoire and Laurent Théry. 2006. A purely functional library for modular arithmetic and its application to certifying large prime numbers. In International Joint Conference on Automated Reasoning. 423–437.
[16]
Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, and Tat Thang Nguyen. 2017. A formal proof of the Kepler conjecture. In Forum of mathematics, Pi. 5.
[17]
Thomas C Hales. 2005. A proof of the Kepler conjecture. Annals of mathematics, 1065–1185.
[18]
Thomas C Hales. 2007. The Jordan curve theorem, formally and informally. The American Mathematical Monthly, 114, 10 (2007), 882–894.
[19]
John Harrison. 2009. Formalizing an analytic proof of the prime number theorem. Journal of Automated Reasoning, 43, 3 (2009), 243–261.
[20]
John Harrison. 2009. HOL light: An overview. In International Conference on Theorem Proving in Higher Order Logics. 60–66.
[21]
Marijn Heule, Warren Hunt, Matt Kaufmann, and Nathan Wetzler. 2017. Efficient, verified checking of propositional proofs. In International Conference on Interactive Theorem Proving. 269–284.
[22]
G Higman. 1940. The Units of Group Rings. Londres. Proc. London Math. Soc, 46 (1940).
[23]
F Immler. 2018. A Verified ODE Solver and the Lorenz Attractor. J Autom Reasoning, 61 (2018), 73–111.
[24]
Irving Kaplansky. 1970. “Problems in the theory of rings” revisited. The American Mathematical Monthly, 77, 5 (1970), 445–454.
[25]
Matt Kaufmann and J Strother Moore. 1996. ACL2: An industrial strength version of Nqthm. In Proceedings of 11th Annual Conference on Computer Assurance. COMPASS’96. 23–34.
[26]
Jannis Limperg and Asta Halkjæ r From. 2023. Aesop: White-Box Best-First Proof Search for Lean. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. 253–266.
[27]
Per Martin-Löf and Giovanni Sambin. 1984. Intuitionistic type theory. 9, Bibliopolis Naples.
[28]
Patrick Massot, Floris van Doorn, and Oliver Nash. 2022. Formalising the h -principle and sphere eversion. arXiv preprint arXiv:2210.07746.
[29]
The mathlib Community. 2020. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020). Association for Computing Machinery, New York, NY, USA. 367–381. isbn:9781450370974 https://doi.org/10.1145/3372885.3373824
[30]
Norman Megill and David A Wheeler. 2019. Metamath: a computer language for mathematical proofs. Lulu. com.
[31]
Dale Miller and Gopalan Nadathur. 2012. Programming with higher-order logic. Cambridge University Press.
[32]
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean theorem prover (system description). In International Conference on Automated Deduction. 378–388.
[33]
Leonardo de Moura and Sebastian Ullrich. 2021. The lean 4 theorem prover and programming language. In International Conference on Automated Deduction. 625–635.
[34]
Alan G Murray. 2021. More counterexamples to the unit conjecture for group rings. arXiv preprint arXiv:2106.02147.
[35]
Adam Naumowicz and Artur Kornił owicz. 2009. A brief overview of Mizar. In International Conference on Theorem Proving in Higher Order Logics. 67–72.
[36]
Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. 2002. Isabelle/HOL: a proof assistant for higher-order logic. Springer.
[37]
U Norell. 2009. Dependently Typed Programming in Agda, Advanced Functional Programming, P. Koopman, R. Plasmeijer, and D. Swierstra (Eds.), Vol. 5832 of LNCS.
[38]
Donald S Passman. 2011. The algebraic structure of group rings. Courier Corporation.
[39]
Christine Paulin-Mohring. 2015. Introduction to the calculus of inductive constructions.
[40]
Lawrence C Paulson. 1989. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5, 3 (1989), 363–397.
[41]
T. Peterfalvi. 2000. Character Theory for the Odd Order Theorem. Cambridge University Press. https://doi.org/10.1017/CBO9780511565861
[42]
S David Promislow. 1988. A simple example of a torsion-free, non unique product group. Bulletin of the London Mathematical Society, 20, 4 (1988), 302–304.
[43]
Robert Sandling. 1981. Graham Higman’s thesis “Units in group rings”. In Integral representations and applications. Springer, 93–116.
[44]
Peter Scholze. 2022. Liquid tensor experiment. Experimental Mathematics, 31, 2 (2022), 349–354.
[45]
Daniel Selsam, Sebastian Ullrich, and Leonardo de Moura. 2020. Tabled typeclass resolution. arXiv preprint arXiv:2001.04301.
[46]
Morten Heine B Sørensen and Pawe l Urzyczyn. 1998. Curry-Howard Isomorphism. Univ. of Copenhagen, Univ. of Warsaw.
[47]
Laurent Théry and Guillaume Hanrot. 2007. Primality proving with elliptic curves. In International Conference on Theorem Proving in Higher Order Logics. 319–333.
[48]
The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book Institute for Advanced Study.

Cited By

View all
  • (2024)Mathematical reasoning and the computerBulletin of the American Mathematical Society10.1090/bull/183361:2(211-224)Online publication date: 15-Feb-2024

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs
January 2024
290 pages
ISBN:9798400704888
DOI:10.1145/3636501
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 January 2024

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Automated Theorem Proving
  2. Dependent Type Theory
  3. Interactive Theorem Proving
  4. Kaplansky's conjectures
  5. Lean theorem prover
  6. group rings

Qualifiers

  • Research-article

Conference

CPP '24
Sponsor:

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)140
  • Downloads (Last 6 weeks)23
Reflects downloads up to 21 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2024)Mathematical reasoning and the computerBulletin of the American Mathematical Society10.1090/bull/183361:2(211-224)Online publication date: 15-Feb-2024

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media