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