16.04.2019 | Ausgabe 4/2020

Homogeneous Length Functions on Groups: Intertwined Computer and Human Proofs
- Zeitschrift:
- Journal of Automated Reasoning > Ausgabe 4/2020
Wichtige Hinweise
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Abstract
We describe a case of an interplay between human and computer proving which played a role in the discovery of an interesting mathematical result (Fritz et al. in Algebra Number Theory 12:1773–1786, 2018). 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.