Arthur Tilley

Stream: new members

[Arthur Tilley]

Hi everyone,

Just want to introduce myself since I'm new to Lean and have been doing a bit of a deep dive over the past few weeks.

Also, I'm about 90% of the way toward formalizing Banach-Tarski (https://github.com/aetilley/banach-tarski). Although the code needs to be cleaned up a lot. (I didn't even know the linter existed when I started the project, then I decided to keep it off for a while to maintain momentum). I'm sure there's a lot in there that I didn't do the ideomatic way, but I'm learning quickly and having a blast.

Feel free to reach out. Cheers.

[Yan Yablonovskiy 🇺🇦]

Welcome!

I had a brief look at your code, and one thing i think you'd love to learn about i didnt see an occurrence of is docs#simpa , which i believe is kind of like the combination simp [foo,bar] at baz; simp [baz] (which would be simpa [foo,bar] using baz ) . For example, in line 193 of BanachTarski/Basic.lean the proof can be:

    have rhs: x ∈ f (gLM y)⁻¹ '' AMs w := by
      simp
      use z
      simpa [f,z] using mem2

[Arthur Tilley]

@Yan Yablonovskiy 🇺🇦

Indeed. I didn't get into the habit of using simpa until late. It is in there a few times though.

I also think I backtracked on simpa a few times at the start because I forgot that, although "rwa" uses "at" syntax (ie. "rwa [h] at a") , "simpa" uses "using" syntax like in your example.

[Christian Krause]

Hi :wave: ,
Good to see that you are also working on Banach Tarski! I had a go at it 2 years ago but abandoned it for locale theory. Recently I picked it up again and decided to start from scratch (whenever I find time...). Mathlib now has a good definition of equidecomposability docs#Equidecomp. There is still some work needing to be done (there was some discussion you might find interesting at #30330). This result for FreeGroups docs#FreeGroup.Orbit.duplicate is also interesting for banach tarski.
I am currently working on proving that F_2 is isomorphic to a subgroup of SO3.
(I can't take a deeper look at your codebase right now but I will certainly do that).

[Arthur Tilley]

Hi @Christian Krause

Very cool. (I did do a web search for BT lean projects before starting out, but did not see yours for some reason.)

And yeah the free subgroup result you mention was an absolute slog, but here it is (main result at the bottom of that file)
and associated lemmas

Apologies in advance for the proofs that are not "pruned" so to speak. Nor is is much commented. The goal for now is to cut my way through then do another pass and make everything nice.

The end is definitely in sight, but one last annoying task remaining is a proof that the Rodrigues matrices (for an arbitrary axis and angle) are in SO(3). When I try to prove the goals of A^T * T = 1 and det A = 1, I get an intractable mess. It would seem this might be a problem someone has already tackled. I'm not sure if you know anything about that?

See proof stub here

[Christian Krause]

I tried tried to avoid that problem by using two concrete matrices: https://github.com/Bergschaf/lean-banach-tarski/blob/11d23ef7bd2a1b5caa3aaf9bcc6d64c4a362e76f/LeanBanachTarski/Definitions.lean#L30

[Arthur Tilley]

Christian Krause said:

I tried tried to avoid that problem by using two concrete matrices: https://github.com/Bergschaf/lean-banach-tarski/blob/11d23ef7bd2a1b5caa3aaf9bcc6d64c4a362e76f/LeanBanachTarski/Definitions.lean#L30

The characterization of SO(3) matrices as Rodrigues matrices is not for the purposes of finding the free subgroup (For that I too used the concrete Sato matrices. That theorem is done.).

The Rodrigues characterization is for the purpose of showing that one can find a member of SO(3) that avoids taking a countable set of points on the unit sphere to itself. This is traditionally done by appealing to the fact that members of SO(3) are really rotations by some angle along some axis.

The rotation matrix representation is fairly common, and I'd be surprised if somebody somewhere hadn't already proved in Lean that they are in SO3 (and vice versa). I will ask in a different channel in a couple days.