## Updates on learning Lean

I have now made it all the way to the end of the metric spaces chapter of the MIL, which means in principle, I should have everything I needed from the book to start the \(Out(F_n)\) project. The last exercise in the section was formalizing a proof that a complete metric space is Baire, a theorem I had not thought about since my undergraduate topology class. Writing down the proof made clear some of the pain points I'm likely to encounter when proving more substantial results.

- The
`simp`

tactic can only do so much: given a goal of the form \(A \cap f(n) \subseteq B \cap f(n)\), where \(f n\) is an indexed family of sets, and we have amongst our hypotheses \(A \subseteq B\), one would expect`simp`

to easily close the goal. However, it made no progress, and it's unclear whether it was the indexing on the family`f`

that threw it off, or it was something else. In any case, I will have a lot of 'almost' trivial goals like this, that I'd like to close automatically, but I will have to do them manually, or someone will have to write a more clever tactic. - A related pain point is more of an ergonomic one: when diving into proofs of these 'almost' trivial subgoals, I would like to fold their proofs after they're completed, so that they don't clutter the main body of the proof. This would be a fairly simple VS Code plugin, if someone choses to do it. On the other hand, perhaps this is a good thing, encouraging proof/code golfing?
- I need a good way to find lemmas related to a specific object: GPT is not doing it any more, since it can really only handle the basic lemmas. The search on Mathlib docs is a little slow, plus there does not seem to be a good way to filter down to lemmas using some sort of semantic search/filtering.

## Some more tactics

`field_simp`

: As the name suggests, this simplifies terms living in a field to a normal form.`linarith`

can be provided helper lemmas to aid in simplification via`linarith [p1, p2, p3]`

.`trans`

: Used to prove goals that are transitive relations. Given a goal`s \sim t`

,`trans u`

will create two subgoals`s \sim u`

and`u \sim t`

.`intros`

: Repeated use of`intro`

until quantifiers in goal are gone.`constructor`

: If the goal is structure with several components, e.g. an AND statement, it will create a goal for each field in the original goal.`congr`

and`gcongr`

: These are congruence tactics, which as far as I understand, are useful when working with group/ring/whatever isomorphisms, and arguments based on applying isomorphisms.`aesop`

: This is a more powerful version of`simp`

, with better proof search algorithms. An example of this is the`continuity`

tactic.`choose`

and`choose!`

: These two tactics essentially convert a complex hypothesis asserting existence of objects satisfying certain properties to functions that construct those objects, and hypotheses that the constructed objects must satisfy.`Nat.le_induction`

and`Nat.strong_induction`

: These are alternate recursors for`Nat`

, which can be used with the`induction`

tactic to start induction at a positive`Nat`

, or do strong induction.

## Preparing for the \(\mathrm{Out}(F_n)\) project

The first step, before actually writing any code, would be to figure out what's already in mathlib that I will need.

- Groups with presentations: Presented group
- Metric spaces and covering spaces, specifically graphs: Metric spaces
- Group actions on metric spaces via isometries: Group actions by isometries
- Gromov hyperbolic groups and spaces: Search on Google and Zulip doesn't turn up much, but asking people in the community might help point to some Github repo that has bits of these implemented.
- PL structures: Unclear if this will be helpful in defining a PL structure on Outer Space.

### Organizing code

- Naming conventions: Refer to this more thoroughly once I start uploading code on Github.
- Documentation conventions: Also refer to this when uploading code to Github, as well as sending PRs to mathlib.
- Library style guidelines
- Sections and variables
- Namespaces

## On typeclass inference

- The syntax
`[Group G]`

(or similar), isn't exactly a typeclass constraint as much as it is an implicit typeclass argument. The difference between this and implicit arguments of the form`{...}`

is that in the`[...]`

case, it uses a typeclass resolution algorithm to find the right instance, but it can possibly be provided a custom instance if the right instance is not found.

## Notes on learning Lean (2/?)

## On how Lean gave me the hypotheses I needed to prove a correct theorem

Working my way through Mathematics in Lean, I came across an exercise that required proving the standard monomial summation identities, e.g. \(\sum_{i=1}^{n} i = \frac{n(n+1)}{2}\), and \(\sum_{i=1 …

read more## Notes on learning Lean (1/?)

Now that I am almost done with my dissertation, I have decided to switch focus and concentrate on doing math that can be formally checked by the Lean Theorem Prover. The ideal sub-field of math for me to start formalizing would be Teichüller theory, and results on mapping class groups …

read more