u/AlpUzman

Hey folks! I am starting a new mini-course on proofs in elementary linear algebra. The target audience is primarily those students who have taken a computation based linear algebra course and now are transitioning to a proof-based linear algebra course. Instead of developing linear algebra theory, we will focus on constructing proofs and writing proofs. Consequently we won't develop the theory much beyond elementary properties of linear transformations.

I am planning to follow Chapter 17 of Chartrand-Polimeni-Zhang; this is an "online only" chapter and is available at https://media.pearsoncmg.com/cmg/pmmg_mml_shared/Chartrand_4e/index.html . I will specifically solve as many problems from there as possible.

If this sounds like something you would benefit from following, here is the github repo I'll be using as the course webpage:

https://github.com/AlpUzman/Proofs_in_Elementary_Linear_Algebra

And I'll add the episodes to the following Youtube playlist:

https://www.youtube.com/playlist?list=PL40ydqvvyXfMwFmNvppWUuE3sgOP1RI5-

On Github so far there is only the 'sittybos' (Greek equivalent of 'syllabus'). I have recorded the first episode already, and I am planning to finish post-production and release it on my Youtube channel in about a week. The mini-course will be freely available on my Youtube channel, with a new episode every other week (tentatively).

I am also attaching a random still from episode 1 as a teaser.

Thanks!

Hey folks!

Finally I released episode 5 of my playthrough of the Natural Number Game. In this episode I prove a bunch of properties of exponentiation (corresponding to the Power World in the game). Here is the link:

https://www.youtube.com/watch?v=YWmHv_JLAw0

Let me know what you think!

Hey folks!

In an earlier post in this subreddit I had mentioned my playthrough of the Natural Number Game. I just released the fourth episode, in which I started and finished the Multiplication World. Here is the link:

https://www.youtube.com/watch?v=YfNuXT118qQ

Let me know what you think!

Hey!

I'm a math phd who completed his training with no exposure to Lean, and more generally my studies and interests have not been near foundations, formalization etc..

To warm up to Lean and for education and entertainment purposes, this summer I started a playthrough the Natural Number Game (Lean 4 version). As I play through the game I take my time expanding on the mathematical (and sometimes philosophical) ideas.

If this sounds like something you would be interested in, feel free to check out the playlist on Youtube:

https://www.youtube.com/playlist?list=PL40ydqvvyXfMpiFcO3-zemMQiWHexecYn

So far I released three episodes, the fourth episode will be out shortly.

After the NNG playthrough is finished, I am planning to play through the other Lean games, and eventually do walkthrough and oneshot speedruns also. (A "oneshot speedrun" is an idea I came up with: basically this requires that the player stays in the typewriter mode, and writes down the whole combo of tactics that would constitute a proof before executing. The syntax that allows this is to use ;'s to chain tactics.)

Hey folks,

About a month ago a counterexample to the long-standing open problem Jacobian Conjecture was found using AI. Pretty much since then I've been working on an explainer video, and I am happy to announce that it's finally up!

The video is a presentation mostly aimed for an audience that is comfortable with multivariable calculus.

Still, I start off at the calculus-zero level, and try to give a non-technical description. This CALC 0 level also includes some thoughts on whether or not AI can replace mathematicians.

Then I transition to the CALC 3 level. First I review most concepts involved, and go on to describe how one might verify that the counterexample by hand. Specifically, based on Terry T's digestion I present a factorization that perhaps makes the constancy of the Jacobian less mysterious.

Next I go one step further and give a discussion at what I call the CALC 5 level; this section is for those comfortable with proof based multivariable calculus.

Throughout I don't use any algebraic geometry, or even complex numbers.

If this sounds like something you would be interested in, here is the link:

https://www.youtube.com/watch?v=MOmLr4DIlEo

It's certainly the most ambitious video I made so far, let me know what you think!