Projects

Stream: LFTCM 2024

[davidlowryduda]

I list the project proposer and a brief description

• @Riccardo Brasca FLT3: formalize the proof of Fermat's Last Theorem for exponent 3 using Eisenstein integers zulip thread
• @Filippo A. E. Nuccio CantorSet: properties like equivalent definitions, 1/4 is in it, compactness
• @Filippo A. E. Nuccio GroupReps: semisimplicity of group reps, irreducible reps of dihedral
• @Filippo A. E. Nuccio Octonions: Cayley-Dickson construction, and their properties (e.g. not associative, but power associative)
• @Chris Birkbeck GLnFq: Counting elements in $GL(n, \mathbb{F}_q)$ zulip thread
• @Chris Birkbeck PowerResidue: Power residue symbols, defined here, and how they interact with residue fields and roots of unity; (this is a preamble to class field theory) zulip thread
• @María Inés de Frutos Fernández Ostrowski: Ostrowski's theorem for global field (classifying all absolute values): there is a partial version in lean3, but it's not in mathlib or lean4 zulip thread
• @Jireh Loreaux StoneWeierstrrass: Stone-Weierstrass for locally compact spaces zulip thread
• @Jireh Loreaux SpectralTheorem: Spectral theorem for normal endomorphisms over $\mathbb{R}$ or $\mathbb{C}$ in finite dimensions zulip thread
• @Jireh Loreaux Reproducing kernel Hilbert spaces (not in mathlib at all)
• @Jireh Loreaux Continuous functional calculus for selfadjoint matrices zulip thread
• @Frédéric Dupuis HilbertTrace: Define the trace in infinite dimensional Hilbert spaces
• @Alessandro Iraci Schur: Schur functions (special symmetric polynomials) --- want to prove an equivalence of determinant definitions zulip thread
• @Anatole Dedecker ProperGroupActions: putting the right defintion of proper group actions into lean, possibly following Bourbaki's definitions zulip thread
• @Vincent Beffara Talagrand: Talagrand's isometric property. (See also this other thread)
• @Sam van G has additional projects on Stone Duality that he's going to mention in his Monday afternoon talk. See this thread

[Etienne Marion]

I would like to work on proper group actions!

[Jireh Loreaux]

One more that should be quite easy:

• @Jireh Loreaux Continuous functional calculus for selfadjoint matrices over ℝ or ℂ.

[Marco Lenci]

@Vincent Beffara Are you getting collaborators for the project on Talagrand's isoperimetric property? I'd ike to jojn, but I'm rather the beginner in Lean...

[Vincent Beffara]

Marco Lenci said:

Vincent Beffara Are you getting collaborators for the project on Talagrand's isoperimetric property? I'd ike to jojn, but I'm rather the beginner in Lean...

Not yet :-(

[Harald Helfgott]

Here's something I have been wondering about: what about running a sieve of Eratosthenes on all integers up to N, for N=10^6, or N=10^9, and producing a proof that the resulting array tells you the truth about the primes up to N?

[Harald Helfgott]

It turns out that there was a discussion on this matter some time ago, but it petered out after a while, for no apparent reason: https://leanprover-community.github.io/archive/stream/270676-lean4/topic/Checking.20the.20Goldbach.20conjecture.html

[Harald Helfgott]

I've just attempted to restarted, making some points at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Checking.20the.20Goldbach.20conjecture

TL;DR: coding a sieve of Eratosthenes in Lean, considered as a functional programming language, is a known exercise. The challenge (which seems to me to be realistic - perhaps I am being naive) consists in producing a proof that the array or list produced is telling you the truth.

[Harald Helfgott]

Note there's already an interesting reply in that thread (extrinsic proof vs. intrinsic proof).