David Moore

Where I'm at right now, will certainly add more books by the end of the month.

🥳

Automated proof checking language .mm files, not a general purpose database. Metamath is old-but-gold youtube.com/watch?v=OOF4NWRy…

There is something deeply, deeply funny to me about the way metamath databases look. "Yes, hi there, wrel, cdm, wss, oh and ACZADFBEZAHZABIUC"

oh boy almost math time

Woo. 's alright. I held back from doing too many back and forths. mathandcode.com/share/11-05-…

Oh interesting. Yeah for my particular post I meant to emphasize it was my own misconception, not an answer to your original question. I can't give a high confidence answer, it sounds like a cool question. I guess, wouldn't the Taylor series info in some coordinate patch live in the symmetric product of cotangent spaces? Since it's a sum like the following picture (f_{,i} = \partial_i f(x) evaluated at x=0). I think if I tried to get to the bottom of it I'd end up responding to things that are ultimately the mistakes of the translation software, maybe I already have! 😆 but it's fun to think about

Read 'em and weep, I now have a monopoly on Vampire Weekend parody songs about learning Metamath.

Who's gonna tell him...

Going over quiz questions from college. Back when I was learning mechanics I'd have done 8 pages of explicit matrix garbage to answer this, now it's like "oh yeah there's a commutator and it's simple once you diagonalize." This was a quals flashcard I quite like.