Homogeneous length functions on groups: intertwined computer and human proofs

DOI10.1007/S10817-019-09523-1MaRDI QIDQ1984792zbMATH OpenOpenAlexWikidataFDO

Authors Siddhartha Gadgil

Publication date 7 April 2020

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

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)

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.

Recommendations

• Computer proofs in group theory
• scientific article; zbMATH DE number 934902
• Computer-assisted discovery and proof
• Computer and Human Reasoning: Single Implicative Axioms for Groups and for Abelian Groups
• The challenge of computer mathematics

Cites work

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

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)