# Homogeneous length functions on Groups: Intertwined computer & human proofs

## TL;DR

This paper discusses a unique collaboration between human mathematicians and computer-generated proofs, leading to the discovery of a significant mathematical result through an iterative process of understanding and abstraction.

## Contribution

It introduces a novel proof methodology combining computer-generated and human-readable proofs to facilitate mathematical discovery.

## Key findings

- Computer-assisted proofs can be effectively understood and generalized by humans.
- The interplay between human insight and computer proofs can lead to new mathematical results.
- A key lemma was derived through this collaborative proof process.

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