Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit Conjecture
| dc.contributor.author | Gadgil, Siddhartha | en_US |
| dc.contributor.author | TADIPATRI, ANAND RAO | en_US |
| dc.contributor.department | Dept. of Mathematics | en_US |
| dc.coverage.spatial | New York | en_US |
| dc.date.accessioned | 2025-04-19T07:34:36Z | |
| dc.date.available | 2025-04-19T07:34:36Z | |
| dc.date.issued | 2024-01 | en_US |
| dc.description.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. | en_US |
| dc.identifier.citation | CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 177 - 189. | en_US |
| dc.identifier.doi | https://doi.org/10.1145/3636501.3636947 | en_US |
| dc.identifier.isbn | 979-8-4007-0488-8 | |
| dc.identifier.sourcetitle | CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs | en_US |
| dc.identifier.uri | https://doi.org/10.1145/3636501.3636947 | |
| dc.identifier.uri | http://dr.iiserpune.ac.in:8080/xmlui/handle/123456789/9652 | |
| dc.language.iso | en | en_US |
| dc.publication.originofpublisher | Foreign | en_US |
| dc.publisher | Association for Computing Machinery | en_US |
| dc.subject | Mathematics | en_US |
| dc.subject | 2024 | en_US |
| dc.title | Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit Conjecture | en_US |
| dc.type | Conference Papers | en_US |