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

TADIPATRI, ANAND RAO; Gadgil, Siddhartha

dc.contributor.author	Gadgil, Siddhartha
dc.contributor.author	TADIPATRI, ANAND RAO
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
dc.identifier.citation	CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 177 - 189.	en_US
dc.identifier.isbn	979-8-4007-0488-8
dc.identifier.uri	https://doi.org/10.1145/3636501.3636947	en_US
dc.identifier.uri	http://dr.iiserpune.ac.in:8080/xmlui/handle/123456789/9652
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.language.iso	en	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
dc.contributor.department	Dept. of Mathematics	en_US
dc.identifier.doi	https://doi.org/10.1145/3636501.3636947	en_US
dc.identifier.sourcetitle	CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs	en_US
dc.publication.originofpublisher	Foreign	en_US