This work was an interplay between human and computer proving which played a role in the discovery of an interesting mathematical result. The unusual feature of the use of computers here was that a computer generated but human readable proof was read, understood, generalized and abstracted by mathematicians to obtain the key lemma in an interesting mathematical result.

The mathematical result proved became PolyMath 14 and was a collaboration on Terence Tao’s blog. The work started with Tao’s posting of a question which was asked to him by Apoorve Khare – whether there was a homogeneous length function on free groups. We (collaboratively) obtained a result which answered the question and went much beyond this, giving a classification of homogeneous pseudo-lengths on all groups.

Faculty: Siddhartha Gadgil

References:

Siddhartha Gadgil: “Homogeneous Length Functions on Groups: Intertwined Computer and Human Proofs”, Journal of Automated Reasoning (2020)64:677–68

Fritz, T., Gadgil, S., Khare, A., Nielsen, P., Silberman, L., Tao, T.: “Homogeneous length functions on groups.”, Algebra Number Theory 12, 1773–1786 (2018)