geometric algebra

Stream: new members

[Robert Webb Jr.]

Hello and thanks for helping with Lean.
I am undertaking to learn Geometric Algebra {ala David Hestenes) and I recognize that it may be most efficient to learn Linear Algebra first/concurrently (e.g., Alan McDonald's work).
I am an older adult independent learner so I would like to use Lean to "check" the proofs that I produce as I study Linear/Geometric Algebra.
Would one of you fine folks please direct me to the most appropriate resources for learning Lean within the stated context?
Thanks for your time.

[Bryan Gin-ge Chen]

We have a list of resources for learning Lean here.

Just a word of advice, with the current state of the art, it will most likely be extremely difficult to simultaneously learn a piece of new math while formalizing it. In most people's experience (though there may be one or two exceptions...), understanding the math inside and out is a necessary prerequisite before attempting a formalization of it.

[Robert Webb Jr.]

Thank you, Bryan. So are there any means for automated proof checking of student proofs? Or is this just a pipe dream?

[Bryan Gin-ge Chen]

It depends on what you mean. Have you tried the Natural Number Game?

[Robert Webb Jr.]

I have Natural Number Game pulled up, but I have not started yet.
By checking student proofs, I mean that when the text says prove that such and so is the case, given the following conditions, I can construct a proof in the theorem prover much as I would on paper (but using prover syntax, of course) and know that my proof is valid because the prover accepts it thus filling the role of instructor. I have thought about using Coq for this, but it seems like Lean might be more accessible.
Anyway, I will see what I can do with what's available.
Thanks again for your time.

[Eric Wieser]

You might be interested in docs#exterior_algebra and docs#clifford_algebra, to get a feel for what is already formalized

[Robert Webb Jr.]

Thank you Eric; I will have a look.

[Eric Wieser]

The answer for mathlib, at least, is currently "really not much", but over at pygae/lean-ga#13 there's a fair bit more

[Robert Webb Jr.]

Thank you, I will have a look there also.

[Eric Wieser]

Lastly, you may be interested in the link I commented on #5059 - I gave a talk at ICCA in collaboration with @Utensil Song to try and sell GA researchers on Lean, and gave a summary of some approaches used to formalize geometric algebra in other theorem provers. You can find it on youtube here: https://m.youtube.com/watch?v=DX2n_-MD-A4

[Robert Webb Jr.]

Excellent.
Thanks for your dedication to GA; my instincts tell me that it is one of the proverbial keys to the kingdom (Homotopy Type Theory being another...).

[Patrick Massot]

You're welcome here but if you believe in homotopy type theory then you should probably learn about another proof assistant.

[Kevin Buzzard]

Yes, lean's axiom system is incompatible with the univalence axiom of homotopy type theory. I wrote a rant recently in another thread arguing that homotopy type theory didn't seem to me to be offering much to formalisation of the kind of mathematics we're interested in here, but of course I am biased!

[Robert Webb Jr.]

Thank you, Patrick.
I am a long ways still from learning HOTT; I just think that it is the correct direction in which to head.
My immediate concern is to get up to speed with Geometric Algebra so that I can apply it to undergrad physics and beyond but McDonald's work is all that I can find that seems targeted toward freshman mathematics and he takes a strict theorem-proof approach but doesn't provide answers in the text, hence my problem...

[Robert Webb Jr.]

Thank you Kevin.