There are two wolves. Just two wolves. Everything we experience as reality arises from relativistic and quantum mechanical interactions of the wolves.
"I've never set a god on fire--"
"--but that one does seem very flammable."
doctor's visit $$$$ help if possible
my neurologist visit is coming up May 10th. It costs $500, and this summer finances are looking really rough.
It's one of the most significant costs in my life. When I had time my Twitch used to cover it, but now I need to ask y'all for some help, if possible.
If you can throw me any help to paying for the doctor's visit my venmo is @Cyborgneticz. My twitch page has a donation link as well.
Anything that goes over will go to meds and hormones
"You know how the \hat command in LaTeΧ puts a caret above a letter? ... Well I was thinking it would be funny if someone made a package that made the \hat command put a picture of an actual hat on the symbol instead?"
And then Matthew Scroggs and Adam Townsend went ahead and did it.
Package at https://ctan.org/pkg/realhats, behind-the-scenes commentary at https://aperiodical.com/2019/03/realhats-writing-a-latex-package/
Thoughts on Coq vs Lean
Unlike in Coq, the programming and theorem proving language are unified, and the syntax feels much more familiar from functional programming. Overall, the design decisions just make a lot more sense to me.
This isn't meant as a critique of the technical merits of Coq--I don't know nearly enough about it for that. But if anyone finds themselves in a similar situation as me where you're put off by the (perceived) idiosyncrasies of Coq, give Lean a try.
Thoughts on Coq vs Lean
A while back I tried to learn Coq. I already had a pretty good grasp of the theory of formal verification, but for some reason I found the nuts and bolts of Coq to be incredibly unnatural. Everything felt clunky to me and cut against the grain of how I liked to think about things. I didn't get very far before I lost motivation to continue.
A few days ago someone recommended I give Lean a shot instead and so far I'm having a lot better luck. 1/
Funny looking equation of the day:
xʸ = yˣ
Solutions for x≠y include (2, 4) (and (4, 2)).
Some history and proofs in Wikipedia https://en.wikipedia.org/wiki/Equation_x%CA%B8%3Dy%CB%A3
math/physics undergrad // he/him // algebraic topology, HoTT, condensed matter, Rust, Haskell
A Mastodon instance for maths people. The kind of people who make \(\pi z^2 \times a\) jokes.
\) for inline LaTeX, and
\] for display mode.