David Moore

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

🥳

Newton's shell theorem or Gauss's law! Make flashcards about it right away! This is a case where the indefinite integrals involved are way more complicated than the final result. There are some cases where you do have to wrestle with integrals like this though, so your work isn't in vain. Volume element is wrong, you either want x=r*[sin(theta) cos(phi), sin(theta)sin(phi), cos(theta)] and volume element r^2 sin(theta) dr dtheta dphi, with an integral from theta=0 to pi, phi=0 to 2 pi. Or you can choose x=r*[cos(theta) cos(phi), cos(theta)sin(phi), sin(theta)] but the volume element will be r^2 cos(theta) dr dtheta dphi and the integral should be taken taken from theta=-pi/2 to pi/2 to cover the whole sphere. With this coordinate stuff fixed, the integral *is* doable, though a bit annoying. This amounts to re-proving Newton's shell theorem though, so you can be proud of yourself for re-deriving Newton's work using modern methods :) (Physics teacher's assistant powers kicking in)

Interesting thing I haven't seen pointed out before: on a lot of Japanese posts, I often see a technical subject-matter post which I feel like begs for interaction, with 500 likes and 0 replies. Has to be some kind of cultural aspect I think.

its joest begun

Fair enough! Yeah what I've been really struggling with is the "philosophy" of it. LLMs *love* to say "this has been mathematically proven," while secretly using unformalized or unformalizable statements. Some weird combo of appeal to authority, prose reward hacking, a strong "intro to proofs" attractor, and worst of all sometimes that's just how logicians actually talk 😆

Noted! Harper ch 1-3 seems GOATed, this is where I'm spending most of my time at the moment. And the metamath book, hanging on every word.

Or that Metamath applies Hilbert-style rules [always] but whether its database described Hilbert-style logic is different... Is there a good web forum for this? Lean Zulip, and Metamath mailing list and github... I'm trying to have more human conversations, and though I'm checking references deeply I'm still bound to end up with wildly weird viewpoints and terminology *somewhere* when indep. studying.

It's been a circuitous path! I've tried learning it in 2013 and several times since but nothing clicked. Certainly these days there's a critical mass of notes and enthusiasm that makes it impossible to ignore. Always happy to talk long-form logic, no way a diet of LLM conversations is healthy for me 😆

👀Heck yeah ty. Yeah my selection of books is quite weird. When I tried to study Lean and Rocq I kept saying "no what is a type? No you're explaining it to me in English, I want to know what is a type?" so writing a Metamath interpreter and bootstrapping through type theory theorems to Lean is the only way for me to go. I'm not even trying to insist on a philosophical position, I just have given up every time I tried to learn that stuff (incl. logic books, model theory, computability) for a decade+, out of confusion, and this is the first time I'm seeing things concretely.

Nice! Yeah as a indep. learner it's so difficult to get the terminology right, I keep having to cite like 5 different books. I'm debating whether to just tell everyone "oh I'm a radical finitist" or whatever just to scare away anyone not making their statements concrete.

You know how the closer you get in expertise to someone the more vehement your disagreements can become? This is how I feel about 95% of what I've read in logic and formal languages. And 100% of things of the form "technically an X is a Y-system not a Z." Like wth those are entirely new English words used informally, I thought we were being formal, aren't you just adding to the pile of things we have to formalize? "Actually in my notation ⊢ is a statement about the existence of a proof not merely [...]" oh really, I must be going crazy, I could have sworn it was a symbol written on a piece of paper. Obviously the way out is just to build things but omg the way the theory is communicated is annoying.

It's a good inequality, sir.

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

every day that ends in y!

$\color{green}{_{\text{this is}}}\color{red}{\text{ GOOD }}^{\color{yellow}\text{news}}$

👀

(not too interesting, I'm sure the BB(5) peeps would have knocked it out in ten minutes)

🥳

I tried solving this but every time I start writing I... I... Zzzzzzzzz