yuppiemephisto

8 ms·

31.
by yuppiemephisto 1y ago
`show_term grind` and `by grind?` should do what you want
32.
by yuppiemephisto 1y ago
What do you think of embedding it in a formal system like Lean as a frontend?
33.
by yuppiemephisto 1y ago
I was surprised to hear their claim about Agda's metaprogramming, I say lean is better here
34.
by yuppiemephisto 1y ago
I don’t know about their motivation, but I would say mine is that Lean is a real programming language. Coq is not really meant for “prosaic” programming, more’s the pity. Lean is also a lot faster.
35.
by yuppiemephisto 1y ago
Maybe too far afield, but: https://leanprover-community.github.io/lean4-metaprogramming... Gives what you wished for. It's functional, though (among other things). Unlike most lisps, (dependently) typed. But hey, avail
36.
by yuppiemephisto 2y ago
> I’d rather have the language … check out Lean 4 then. Its syntax system is based on Racket but —instead of parens— implements stuff like [JSX syntax]( https://github.com/leanprover-community/ProofWidgets4/blob&
37.
by yuppiemephisto 2y ago
Unsurprised. I got the impression Bukele picked bitcoin in a sort of manic ADHD moment and no one pushed him on it, figuring it was their president’s personal indulgence.
38.
by yuppiemephisto 2y ago
If you can get .tex source files, ask GPT to rename the variables to something nicer, including more than one letter long names. Helps.
39.
Which of the classical groups are compact?(alok.github.io)
3 points by yuppiemephisto 2y ago|0 comments
40.
by yuppiemephisto 2y ago
This answer is my favorite. You got it =)
41.
by yuppiemephisto 2y ago
That's what "up to an infinitesimal error anyway" meant.
42.
by yuppiemephisto 2y ago
Certainly I'm glad we have better tools now, and know the rules. Sure beats the old days. As for verification, well I'm big into Lean 4 and it plays well with NSA since transferring theory and proofs between finite and infinite sa
43.
by yuppiemephisto 2y ago
Ok, describe your experience.
44.
by yuppiemephisto 2y ago
Does it work with more obscure languages like Lean 4?
45.
by yuppiemephisto 2y ago
The hyperreals and surreals are actually isomorphic under a mild strengthening of the axiom of choice (NBG). https://mathoverflow.net/questions/91646/surreal-numbers-vs-... See Ehrlich’s answer.
46.
by yuppiemephisto 2y ago
The number N in question will adjust with dx (up to infinitesimal error anyway). So if dx is halved, N will double. But both retain their character as infinitesimal and hyperfinite.
47.
by yuppiemephisto 2y ago
There are theories like SPOT and Internal Set Theory that don’t require filters. Plus the ancient mathematicians did very well with just their intuition. And more to the point, I cared much more about building (hyper)number sense than som
48.
by yuppiemephisto 2y ago
Thanks! And yeah I’m familiar with Nelson
49.
by yuppiemephisto 2y ago
All these would be infinitely close in the nonstandard characterization. I just picked logistic because it was easy and step is discontinuous so it shows off the approach’s power. If I started with delta instead I would have done Gaussian a
50.
by yuppiemephisto 2y ago
See my code at the end. The Wikipedia article is pretty good too. I can send you more if you like.
51.
Derivative at a Discontinuity(alok.github.io)
134 points by yuppiemephisto 2y ago|62 comments
52.
by yuppiemephisto 2y ago
Of all things, The Venture Bros convinced me otherwise that the copies “are” me, enough to matter anyway.
53.
Learn perfect pitch in 15 years(moderndescartes.com)
171 points by yuppiemephisto 2y ago|147 comments
54.
Derivative at a discontinuity(alok.github.io)
2 points by yuppiemephisto 2y ago|1 comments
55.
by yuppiemephisto 2y ago
This uses a simpler approach than generalized functions/distributions.
56.
by yuppiemephisto 2y ago
> The fact everyone that say they've become more productive with LLMs won't say how exactly. But no one really show how they're actually solving problems with LLMs and how the alternatives were worse for them. A pretty lit
57.
by yuppiemephisto 2y ago
Just did! =)
58.
by yuppiemephisto 3y ago
Can do it in pure ZF: https://www.youtube.com/watch?v=YE68yptMMeQ https://u.cs.biu.ac.il/~katzmik/spot.html
59.
by yuppiemephisto 3y ago
https://alok.github.io/2022/09/12/y539043/
60.
by yuppiemephisto 3y ago
Related to the DFT view: https://www.sciencedirect.com/science/article/abs/pii/S00492...

More ›