Homogeneous length functions on groups: intertwined computer and human proofs

DOI10.1007/S10817-019-09523-1zbMATH Open1468.20081arXiv1904.05214OpenAlexW2963899149WikidataQ113901243 ScholiaQ113901243MaRDI QIDQ1984792FDOQ1984792

Siddhartha Gadgil

Publication date: 7 April 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

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. 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.

Full work available at URL: https://arxiv.org/abs/1904.05214

zbMATH Keywords

type theorygeometric group theoryhomotopy type theory

Mathematics Subject Classification ID

Geometric group theory (20F65) Mechanization of proofs and logical operations (03B35) Commutator calculus (20F12) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)

Cites Work

• Watson-Crick pairing, the Heisenberg group and Milnor invariants
• The Hoffmann-Jørgensen inequality in metric semigroups
• Homogeneous length functions on groups

This page was built for publication: Homogeneous length functions on groups: intertwined computer and human proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1984792)