2360124 Proving theorems in Lean 4

We proved 2 theorems:

1. Sorting a permutation.

Let $S_n$ be the set of permutations of ${0,\dots,n-1}$.

Define a function $f\colon S_n \to S_n$ as follows:

$$ f(\pi)(i) = \begin{cases} \pi(\pi(0)-i) & \text{if } i \le \pi(0), \\ \pi(i) & \text{if } i > \pi(0). \end{cases} $$

For every $n$ there exists $m$ such that for all $\pi \in S_n$:

$$ f^{(m)}(\pi)(0) = 0. $$

2. Collatz for polynomials.

We consider polynomials in one indeterminate (x) with coefficients in $\mathbb{F}_2$, the field with two elements ${0,1}$ (addition is XOR). The ring of such polynomials is denoted $\mathbb{F}_2[x]$.

Theorem (Collatz on $\mathbb{F}_2[x]$).
Define a function $f : \mathbb{F}_2[x] \to \mathbb{F}_2[x]$ by

$$ f(P) = \begin{cases} P/x & \text{if } x \mid P, \\ (x+1)P + 1 & \text{if } x \nmid P. \end{cases} $$

If $P \neq 0$, then there exists $n \in \mathbb{N}$ such that

$$ f^{(n)}(P) = 1. $$

Tools We Used

Both projects utilize Lean 4 version lean v4.26.0-rc2. mathlib documentation loogle various LLM models (such as gemini and chatgpt).

Experience

Workflow First, we've read the proof and we made sure that we understand each logical implication. Next, we sat together to define the necessary definitions and the proofs skeleton. Afterwards, we tried to divide the proof to smaller lemmas and we split the work between both of us. We also tried to make a lemma for every nontrivial logical step in the original proof.
For proving each lemma, we had several ways of trying it. First we tried to find if there is already a proof for that, or something similar enough in mathlib - we tried searching in mathlib documentation itself, in loogle or asking an LLM to search for one. Usually the search was unsuccessful and we ended up proving each lemma by unfolding every definition.

Difficulities we encountered One difficulty was getting used to work and do arithmetic with Fin. For example, in g_k_inv lemma, we found it difficult to prove that $$k - (k - i) = i,$$ which wasnt trivial.
Another diffiuculty we had was how to properly prove with nested induction, which wasn't succesful until we added 'generalizing' for the inner induction.