Top

Journal of Automated Reasoning

Published in:

16-04-2019

Homogeneous Length Functions on Groups: Intertwined Computer and Human Proofs

Author: Siddhartha Gadgil

Published in: Journal of Automated Reasoning | Issue 4/2020

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

previous article A Formalized General Theory of Syntax with Bindings: Extended Version

next article Automated Reasoning with Power Maps

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Participants: T. Fritz, S. Gadgil, A. Khare, P. Nielsen, L. Silberman, T. Tao.

https://github.com/siddhartha-gadgil/Superficial/wiki/A-commutator-bound for the full proof as originally posted.

Indeed, an optimal algorithm for \(l_b(g; B)\) for general finite B gives a solution to the word problem for groups, which is known to be algorithmically undecidable. Namely, given relations\(r_1 \in \langle \alpha , \beta \rangle \), \(r_2\in \langle \alpha , \beta \rangle \), ...\(r_m \in \langle \alpha , \beta \rangle \), let B be the set \(\{(r_1, 0), (r_2, 0), \dots , r_n, 0)\}\). Then \(l_b(g; B)= 0\) if and only if g is trivial in the group \(\langle \alpha , \beta ; r_1 = e\), \(r_2 = e, \dots r_m =e \rangle \).

The full code is in the repository https://github.com/siddhartha-gadgil/Superficial. The script is generated from this source. The script uses the same algorithms we originally used, but with modifications to be more robust in memory usage and to avoid concurrency (as the concurrency we implemented leads to non-determinacy, and occasionally to race conditions).

The proof was posted less than two days after we began writing code, and the main question answered less than a day after that.

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

Gadgil, S.: Watson–Crick pairing, the Heisenberg group and Milnor invariants. J. Math. Biol. 59, 123–142 (2009)MathSciNetCrossRef

Khare, A., Rajaratnam, B.: The Khinchin–Kahane inequality and Banach space embeddings for metric groups, preprint (2016)

Khare, A., Rajaratnam, B.: The Hoffmann–Jørgensen inequality in metric semigroups. Ann. Probab. 45, 4101–4111 (2017)MathSciNetCrossRef

Title: Homogeneous Length Functions on Groups: Intertwined Computer and Human Proofs
Author: Siddhartha Gadgil
Publication date: 16-04-2019
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 4/2020
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-019-09523-1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 4/2020

A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm

A Formalized General Theory of Syntax with Bindings: Extended Version

Formalizing the Cox–Ross–Rubinstein Pricing of European Derivatives in Isabelle/HOL

An Assertional Proof of Red–Black Trees Using Dafny

Automated Reasoning with Power Maps

Premium Partner