maxwells-daemon

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 ways I can imagine it doesn't:

- We can reduce warming by other means, like changing the Earth's albedo.

- A lot more energy falls to Earth every day from the sun than we use via petroleum; a good amount of solar/wind would let us climb back up the hill via sequestration.

- We don't need to sequester CO2/methane into high-energy-density hydrocarbons; could an efficient sequestration process yield eventually net positive energy per unit greenhouse gas from the burn -> sequester process?

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 students explore classes they wouldn't have if they had to worry about GPA. I know a few people that changed their whole field as a result; the geology department was known to pick up students this way.

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 because they didn't break a window.

I don't know exactly what legal technicalities are involved, but this did actually happen to me in a de facto sense!

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 "system" (no, not CAGED either). This is the only path to real fluency; imagine having a neat system of remembering what each English word means and having to go through it every time you wanted to speak!

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 map standalone, just sending audio over Bluetooth. Maybe it's possible to get Android Auto or Carplay to reject GPS data from the car? I don't know...

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, but we might lose the greatest artists.

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 won't get enough practice and exposure to make influential work later.

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 heck of a lot of RL on theorem proving, so Aristotle winds up being much better at writing Lean than other coding agents are.

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 all of the common topics very soon!

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 problem to be hard and the proof is very short, you've probably missed something!

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 theorems!

In other fields (topology, probability, linear algebra), many key definitions are not in Mathlib yet, so you will struggle to write down the theorem itself. (But in some cases, Aristotle can define the structure you are talking about on the fly!)

This is not an intrinsic limitations of Lean, it's just that nobody has taken the time to formalize much of those fields yet. We hope to dramatically accelerate this process by making it trivial to prove lemmas, which make up much of the work. For now, I still think humans should write the key definitions and statements of "central theorems" in a field, to ensure they are compatible with the rest of the library.

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 checker, you can prove some very "nonlocal" properties: this system does not deadlock, or it makes progress at least every N steps, etc.

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 correct, Aristotle has a good chance at translating it into Lean (which is a strong vote of confidence that your English proof is solid). I believe that's what happened here.

- Once a proof is formalized into Lean (assuming you have formalized the statement correctly), there is no doubt that the proof is correct. This is the core of our approach: you can do a lot of (AI-driven) search, and once you find the answer you are certain it's correct no matter how complex the solution is.

Happy to answer any questions!

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 exciting to me!)

One is that modern formal systems like Lean are quite concise and flexible compared to what you're probably expecting. Lean provides the primitives to formalize all kinds of things, not just math or software. In fact, I really believe that basically _any_ question with a rigorous yes-or-no answer can have its semantics formalized into a kind of "theory". The proofs are often close to how an English proof might look, thanks to high-level tactics involving automation and the power of induction.

Another is that proof-checking solves what are (in my opinion) two of the biggest challenges in modern AI: reward specification and grounding. You can run your solver for a long time, and if it finds an answer, you can trust that without worrying about reward hacking or hallucination, even if the answer is much too complicated for you to understand. You can do RL for an unlimited time for the same reason. And Lean also gives you a 'grounded' model of the objects in your theory, so that the model can manipulate them directly.

In combination, these two properties are extremely powerful. Lean lets us specify an unhackable reward for an extremely diverse set of problems across math, science, and engineering, as well as a common environment to do RL in. It also lets us accept answers to questions without checking them ourselves, which "closes the loop" on tools which generate code or circuitry.

I plan to write a much more in-depth blog post on these ideas at some point, but for now I'm interested to see where the discussion here goes.

[1] https://leandojo.org/leandojo.html [2] https://aristotle.harmonic.fun/

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't implemented that interface?

(or, perhaps, agents could use web accessibility tools if they're set up, incentivizing developers to make better use of them)

LeanDojo (at least as original published) did not use automatically formalized data, but extracted examples from Mathlib, which is already written in Lean.

Second author here. Happy to answer any questions about the work!

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 hopeful for even more impressive downstream applications, eg robotics.

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 algorithms can.

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).

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 a lot in subroutines of combinatorial optimization, like heuristics for guiding search on subsets of NP-complete problems. The fact that you can automatically evaluate the heuristic and train by RL is also very convenient.

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 I really do think that ML has real potential to customize a design much more "deeply" than traditional automation tools.

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 well as verifying math research. But fully formalizing anything big leads to a proliferation of small annoying lemmas -- not "difficult" to prove per se, just annoying and time-wasting. I'm working on a neural theorem prover that aims to solve these lemmas fully automatically.

[1] https://leanprover.github.io/

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 we're worried about are predicted to show up. I'd caution against projecting the "We were right!" stance to the general public, since it breeds skepticism when some of the models inevitably turn out to be inaccurate. I think this kind of underreporting-of-uncertainty was the source of a lot of public distrust during COVID. The right approach to modeling -- creating multiple models and combining them to get mean and uncertainty estimates -- is what the modelers are doing, but I think it's important to do more nuanced reporting on what makes a climate model "correct" or "useful."

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 midgame with a fast endgame solver [1]. Probably the coolest feature that's currently finished is that valid moves are generated and executed with SIMD instructions, so searching a new position only takes a few clocks on a modern cpu.

[1] https://github.com/maxwells-daemons/reason

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 server mode makes it easy(ish) to integrate with other software.

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.

It's mostly that these are very narrow and shallow networks -- if I remember right, 5 layers and 30 units wide?

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://imgur.com/a/BrNhwkF

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 big gains from reading the textbook ahead of time