A new type of "high-level programming language" that seems really worth trying to make, is a language that gets compiled to Lean (or HOL, or...) that is specifically about making it as friendly as possible for a human to read definitions and theorems. Not the proofs - as all that matters with proofs is that the proofs are correct - just the definitions and theorems. The intended use case is that AI outputs a blob of proofs, and you're trying to make it as easy as possible for anyone reading the output to understand what the actual precise claims are that have been proven
- 8 replies
- 19 recasts
- 111 reactions
New lore dropped: Open weights are not the capital of communism anymore, now Cuba is. So we can all get back to supporting open weights again. https://www.state.gov/cuba-the-capital-of-21st-century-communism/
- 4 replies
- 8 recasts
- 55 reactions
Thread: how I think about the growth of AI capabilities and what it means for us as they keep getting stronger. I think the right model for comparing humans and AI is not any single dimension like intelligence or aggregate performance on economic tasks. Rather, I view both humans and machines as having a whole range of capabilities. This includes both physical (eg. doing things with our hands, walking) and mental (eg. strategic thinking, mental math, emotional intelligence). For most of human history, machines have only exceeded us in very few areas, eg. a strong early example is water and windmills. So we can look at the situation in 1500 like this:
- 8 replies
- 21 recasts
- 108 reactions