Writing proof of the existence of universal Clifford algebra

Stream: new members

[andme.fikri]

Hi, my name is Fikri. I'm an undergraduate student in mathematics. I'm new to Lean. I need to do a final project as a prerequisite to complete my degree. I'm thinking of trying to write a formal proof in Lean 4 for the theorem "Every finite-dimensional quadratic space has a universal Clifford algebra". Do you think this is doable and is a good idea? Thank you :D

[Kevin Buzzard]

There's a big learning curve for lean but if you have the time then sure you can do it. In 11 weeks I get my undergraduates from no lean experience to writing projects at this level, but they have plenty of other people to ask questions to during that time.

[Kevin Buzzard]

Can you state precisely the theorem you want to prove? "Has a universal Clifford algebra" is a bit vague -- exactly what universal property do you want?

[andme.fikri]

It's a theorem from the book Clifford Algebras and the Classical Groups by Ian Porteous published in 1995.

In chapter 15, there is Theorem 15.19 (Existence theorem).

It's only 1 sentence long, that is "Every finite-dimensional quadratic space has a universal Clifford algebra."

[andme.fikri]

I think, in terms of scope as a project, it should be "possible". As it is not too general and not too narrow. But I'd like to know what you think of it.

[Kim Morrison]

It sounds like before proceeding to working out how hard it is to formalize, you should understand that informal statement!

[andme.fikri]

Please pardon me, but since I'm quite new to the field of formalization, I'm not quite sure yet what to distinguish between formal and informal.

If I were able to prove this theorem by hand, is it unreasonable to transfer it to Lean?

Let's assume the best case scenario, where I was to study intensively for 11 weeks as Prof. Buzzard suggest.

[andme.fikri]

However, I'd like to also apologize, as currently I am still in the middle of studying Clifford Algebra, and I have yet to reach chapter 15. So, at the moment, I also am not quite sure what the theorem means. But hopefully I'll get there soon...

[andme.fikri]

I admit that I kind of arbitrarily choose this theorem simply to set as an objective clear goal for myself.

[Kevin Buzzard]

If you don't understand the maths and you also don't know lean then I would not recommend it as a project. My students formalise results which they've learnt in other courses and are confident with mathematically. I had assumed when talking earlier that you knew the complex meaning of the word "universal" in this context.

[andme.fikri]

I see...

The word universal has never come up in the textbook before chapter 15 at all. So, really, I don't know what the word universal in this context means.

I only copied the words of the theorem directly from the book and pasted it when I prompted my question.

I shall find out what this entails first, and I will get back to you.

[Kevin Buzzard]

The issue is that universal algebra is quite complicated and it takes a while to get your head around the informal concept, which you'll need to understand very solidly before you embark on learning how to do universal algebra in the context of a theorem prover. That's why I am discouraging this project (unless you have 6 months to do it). I say again -- the best way to learn how to use a theorem prover is to formalise mathematics which you're really solid on, because believe me learning how to use a theorem prover is quite difficult even when formalising things you informally understand very well

[andme.fikri]

Here's something of an explanation directly from the book,

"A 2^n-dimensional real Clifford algebra for an n-dimensional quadratic space X is said to be a universal real Clifford algebra for X. Since any two universal Clifford algebras for X are isomorphic, and since the isomorphism between them is essentially unique, one often speaks loosely of the universal Clifford algebra for X."

Is this the same kind of universal that you mean?

[Kevin Buzzard]

The question is not what I mean, the question is whether you can just reply to this message and rattle off a proof from first principles that any two universal Clifford algebras are isomorphic, and that the isomorphism is essentially unique, and furthermore explain precisely in mathematical terms what the word "essentially" means here. If not, I would not recommend this as a first formalization project because universal algebra is subtle to do informally and even more subtle to do formally so is not really suitable as first project if you don't have a solid understanding of it. That's all I'm saying and I've said it several times now so probably I've made my point.

[Kevin Buzzard]

(sorry, double-post)

[andme.fikri]

Thank you very much. I understand what you mean now :)

I think I will choose a different theorem to formalize then. One that is simpler and I'm more familiar with. I'll still try to pick one from Clifford algebra.

In terms of time, technically I have about 16 weeks to do this project. Right now, I'm still proposing various ideas for what I can do for the project to my lecturer.

[Andrés Goens]

@andme.fikri do you have someone at your university that will supervise you on this project? Maybe they have some suggestions of what a suitable project would be, and you can discuss and weigh up the options with them

[andme.fikri]

Yes, currently there is one person who'll be supervising me on the project.

[r.z. Almi.]

andme.fikri said:

Hi, my name is Fikri. I'm an undergraduate student in mathematics. I'm new to Lean. I need to do a final project as a prerequisite to complete my degree. I'm thinking of trying to write a formal proof in Lean 4 for the theorem "Every finite-dimensional quadratic space has a universal Clifford algebra". Do you think this is doable and is a good idea? Thank you :D

• "as prerequisite to complete my degree", necessity is a weak reasoning paradigm.
• the premise of the question is unbounded and thus the conclusion is free.

Good luck.

[Eric Wieser]

andme.fikri said:

Here's something of an explanation directly from the book,

"A 2^n-dimensional real Clifford algebra for an n-dimensional quadratic space X is said to be a universal real Clifford algebra for X. Since any two universal Clifford algebras for X are isomorphic, and since the isomorphism between them is essentially unique, one often speaks loosely of the universal Clifford algebra for X."

Is this the same kind of universal that you mean?

My reading of this is that this is just describing docs#CliffordAlgebra itself; though mathlib doesn't know that the result is 2^n dimensional (and this is a bad project because there are open PRs that already work towards this which need review, not redoing from scratch!)

[Eric Wieser]

Using the terminology of Porteous, CliffordAlgebra Q is "the universal Clifford algebra" for a quadratic space described by Q.

[Eric Wieser]

andme.fikri said:

I think I will choose a different theorem to formalize then. One that is simpler and I'm more familiar with. I'll still try to pick one from Clifford algebra.

I don't have a huge amount of time, but can try to help with this; I'm afraid I already picked off much of the low-hanging fruit for Clifford algebras in my PhD thesis!

[andme.fikri]

Hi, thank you so much! Do you have any recommendations on what theorem I can attempt to formalize? One that's reasonably feasible for someone new like myself.

[andme.fikri]

Although, since this is an undergraduate project and the objective is to learn, my lecturer said that it is alright to simply attempt to formally prove the basic properties of the Clifford algebra, to limit the scope. If I were to go for something more complicated, that can be explored later on after I finish the project.

[Notification Bot]

This topic was moved here from #lean4 > Writing proof of the existence of universal Clifford algebra by Eric Wieser.

[Eric Wieser]

A reasonably feasible goal would be to formalize some more isomorphisms of Clifford algebras; I've done the real / complex / quaternions, but there are some matrix isomorphisms that I didn't go near

[Eric Wieser]

That is, you could fill out some entries in the table at https://en.wikipedia.org/wiki/Classification_of_Clifford_algebras#Classification

[Eric Wieser]

Chapter 10 of my thesis should outline a fairly reusable strategy for doing so

[Eric Wieser]

$\operatorname{Cl}_{p+1,q+1}(\mathbf{R}) = \mathrm{M}_2(\operatorname{Cl}_{p,q}(\mathbf{R}))$ might be a good main target

[Eric Wieser]

Though you could do the simpler $\operatorname{Cl}_{1,1}$ first for practice

[andme.fikri]

This is definitely an awesome objective to pursue :D

Thank you, I'll discuss this with my lecturer first as a proposal.

I'll let you know if there are further updates!

[andme.fikri]

Hi, I've talked with my lecturers. They have agreed to let me do this as my project. Hopefully I will have 2 people supervising my progress.

Right now, I'm in the process of writing down the proposal. Afterwards, I'll just need to get it approved.

I'd like to thank you for helping me choose this topic :D

[andme.fikri]

Hi, so my final project proposal has been approved!

[andme.fikri]

I've budgeted my effective time to work on it for 16 weeks.

[andme.fikri]

I guess, this will be my entire life for the time being... ;)