HackerPapers

arXiv:1509.05468math.GR

Loops with abelian inner mapping groups: An application of automated deduction

Michael Kinyon, Robert Veroff, Petr Vojtěchovský

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

Abstract

We describe a large-scale project in applied automated deduction concerned with the following problem of considerable interest in loop theory: If $Q$ is a loop with commuting inner mappings, does it follow that $Q$ modulo its center is a group and $Q$ modulo its nucleus is an abelian group? This problem has been answered affirmatively in several varieties of loops. The solution usually involves sophisticated techniques of automated deduction, and the resulting derivations are very long, often with no higher-level human proofs available.

arXiv comments
Journal reference
Automated Reasoning and Mathematics, Essays in Memory of William McCune, Lecture Notes in Artificial Intelligence 7788 (editors Maria Paola Bonacina and Mark E. Stickel), Springer 2013, pp. 151-164
DOI
Subjects
math.GRGroup Theory

On Hacker News

Linked by 1 identifiable commenter in 2 comments across 2 threads, from Jun 2017 to Sep 2017.

Comments linking this paper, per year.

Discussed in comments2 threads

  1. Baffling ABC maths proof now has impenetrable 300-page ‘summary’ 1 comment

    • Indeed. We now actually have some math results of interest for which we have only formal proofs and no human proofs. https://arxiv.org/abs/1509.05468 is an example.

      sanxiynView on HNParent context

  2. Automated Theorem Proving in Quasigroup and Loop Theory (2010) [pdf] 1 comment

    • For more recent result of automated theorem proving in loop theory, see "Loops with abelian inner mapping groups: An application of automated deduction (2015)". https://arxiv.org/abs/1509.05468

      sanxiynView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.