Please use this identifier to cite or link to this item:
http://dr.iiserpune.ac.in:8080/xmlui/handle/123456789/9652| Title: | Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit Conjecture |
| Authors: | Gadgil, Siddhartha TADIPATRI, ANAND RAO Dept. of Mathematics |
| Keywords: | Mathematics 2024 |
| Issue Date: | Jan-2024 |
| Publisher: | Association for Computing Machinery |
| Citation: | CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 177 - 189. |
| 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. |
| URI: | https://doi.org/10.1145/3636501.3636947 http://dr.iiserpune.ac.in:8080/xmlui/handle/123456789/9652 |
| ISBN: | 979-8-4007-0488-8 |
| Appears in Collections: | CONFERENCE PAPERS |
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.