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.

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!

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)