maxwells-daemon

10 ms·

1.
by maxwells-daemon 1mo ago
Sorry if this sounds like a dumb question, but I legitimately don't know: does the thermodynamic argument hold up? (Broadly, I agree that humanity needs a healthier relationship with industrialism before fixing this is possible). A few
2.
by maxwells-daemon 1mo ago
My college (Caltech) was pass/fail (no quantified grades) for the first couple of terms, and I thought it worked very well. It did alleviate the some of the stress of beginning a higher-expectations environment, but it also let student
3.
by maxwells-daemon 1mo ago
Funny enough, I had some valuable stuff (including my passport!) stolen from my car, which I'd left unlocked because I was moving some heavy boxes. The police in my area (bay area) said they couldn't really do anything about it be
4.
by maxwells-daemon 2mo ago
As someone who also used to overthink memorizing the fretboard: this is a bad idea. You should strive to just plainly memorize the names of all of the notes, the relevant scale and arpeggio patterns, etc, without any kind of tricks or &quot
5.
by maxwells-daemon 4mo ago
I have exactly the same problem in my (latest-model) Honda Civic / Android Auto! I thought I was going crazy, I'm glad to hear someone else has the same problem. The only fix I've found is to disconnect the phone and use its
6.
by maxwells-daemon 7mo ago
It's true, but most of the cultural innovation I'm aware of, from Bach to Coltrane to Hendrix, came from people who could make art their life, largely by paying the bills with it. I don't think we'll lose art entirely, b
7.
by maxwells-daemon 7mo ago
That isn't how it works. Jimi Hendrix, the Beatles, and most other innovators were regular working artists long before they were influential. If you take away the means for artists to sell work that isn't boundary-pushing, they wo
8.
by maxwells-daemon 8mo ago
Aristotle's output is formally verified in Lean, so you can run it for days on a hard problem and be assured that the answer, no matter how complex, is right without needing to manually check it. Claude Code can write lean, but we do a
9.
by maxwells-daemon 8mo ago
Yes! I think that working with Mathlib is the best long term solution, because it's how people already collaborate on building out the formal "universe of mathematics." We want to speed that up, and hopefully we'll cover
10.
by maxwells-daemon 8mo ago
For this reason, when we announce results on e.g. the IMO, we formalize the statements by hand and inspect the proofs carefully to ensure they capture the full spirit of the problem. However, there are some good heuristics. If you expect a
11.
by maxwells-daemon 8mo ago
Thank you! It depends on the topic. Some fields (algebra, number theory) are covered well by Lean's math library, and so I think we are already there; I recommend trying Aristotle for yourself to see how reliably it can formalize these
12.
by maxwells-daemon 8mo ago
We are! We very recently announced some results on formally proving the correctness of programs: https://harmonic.fun/news#blog-post-verina-bench-sota Formal methods are cool because, by contrast to tools like the borrow ch
13.
by maxwells-daemon 8mo ago
I work at Harmonic, the company behind Aristotle. To clear up a few misconceptions: - Aristotle uses modern AI techniques heavily, including language modeling. - Aristotle can be guided by an informal (English) proof. If the proof is correc
14.
by maxwells-daemon 9mo ago
There are a couple of interesting benefits from the machine learning side that I think discussions of this kind often miss. (This has been my field of research for the last few years [1][2]; I bet my career on it because these ideas are so
15.
by maxwells-daemon 2y ago
Maybe there's a middle ground: a site that wants to work as well as possible for agents could present a stripped-down standardized page depending on the user agent string, while the agent tries to work well even for pages that haven&#x
16.
by maxwells-daemon 2y ago
LeanDojo (at least as original published) did not use automatically formalized data, but extracted examples from Mathlib, which is already written in Lean.
17.
by maxwells-daemon 2y ago
Second author here. Happy to answer any questions about the work!
18.
by maxwells-daemon 4y ago
Wow! The ability to ingest the "cross product" of data on the internet and in the real world is huge; I bet a lot of what LMs don't know yet lives in that space. This seems a lot more general-purpose than CLIP, so I'm ho
19.
by maxwells-daemon 4y ago
In general, a function approximation solution like deep learning does worse on cases where exhaustively finding the exact optimum is possible (small combinatorial problems), but can be applied to much larger instances than the exact algorit
20.
by maxwells-daemon 4y ago
I guess so, but the fact of the matter is that ML/AI is actually, right now, doing useful things that would have been impossible 10 years ago. I don't think I could say the same about crypto (as distinct from cryptography).
21.
by maxwells-daemon 4y ago
Yes, the way I see it, one of the major benefits of deep learning is that it lets you define functions (in the R^n -> R^m sense) that would be basically impossible to define with traditional programming techniques. I think this comes up
22.
by maxwells-daemon 4y ago
I work on this team! (Specifically: applied deep learning research, chip design). It's a shame to see so many people dismissing this work as marketing. I see lots of clever people working hard on really novel and interesting stuff, and
23.
by maxwells-daemon 5y ago
Automated theorem proving + neural language models + reinforcement learning. I think most people seriously underestimate how powerful modern proof assistants like Lean [1] are for building things like provably correct software and chips, as
24.
by maxwells-daemon 5y ago
A friend who works in climate modeling recently told me that the best models currently in use pretty much all agree about the next few years, but they seriously diverge after a couple of decades because that's when the emergent effects
25.
by maxwells-daemon 5y ago
Caltech, right? Were you the author of Flippy? There's a new generation of AlphaZero-style ML bots that's managed to finally dethrone it :) I've been working on and off on a Rust Othello bot aiming to combine AlphaZero in the
26.
by maxwells-daemon 5y ago
In my experience: one of Lean's main advantages is developer experience. It's convenient by design, with lots of automation to make easy proofs trivial. You do your work in VSCode or Emacs rather than some outdated IDE, and the se
27.
by maxwells-daemon 5y ago
I use 2x3090 to train large language models, and mine don't thermal-throttle with air cooling even though they're right next to each other. Eth mining does generate too much heat though.
28.
by maxwells-daemon 5y ago
It's mostly that these are very narrow and shallow networks -- if I remember right, 5 layers and 30 units wide?
29.
by maxwells-daemon 5y ago
My desktop background is the output of a neural network with random parameters that maps (x, y) to (r, g, b): https://i.imgur.com/KySV77c.jpg . Here's a small album of other wallpapers I've made like this: https:&
30.
by maxwells-daemon 5y ago
Maybe! But sometimes the professor really does just whiz through some proofs without a lot of pause or explanation, and even when I grok the content, rushing to write it all down was mostly counterproductive. But yeah, I've also seen b

More ›