points by bananaflag 2 days ago | 0 comments
I find it a bit ridiculous that they claim three discoveries in "math, CS, physics" when they are basically all pure math (in particular, they all may be formalized in Lean) and only belong to these different disciplines for historical reasons.
[–] sevenzero 2 days ago
So again farming the low hanging fruits for marketing?
[–] juliusjh 2 days ago
Call these problems "low hanging fruits" may be the understatement of the century.
[–] sevenzero 2 days ago
If everything of this can be represented in Lean, with enough compute, they are low hanging fruits, yes
[–] hkalbasi 2 days ago
So maybe everything is now low hanging fruit, with your definition.
[–] gimlichgu 2 days ago
maybe, or maybe some problems turn out to be reasonably defeatable by educated guess brute forcing with lots of compute and big models pointing the search in reasonable directions.
[–] juliusjh 2 days ago
Yes, maybe what is hard for LLMs and what is hard for humans have a very small overlap. But calling it brute force or low-hanging fruits is still a bit absurd.
You can safely argue that it's statistics, because by construction it is. But then, maybe nothing is anything more than statistics.
[–] saikia81 2 days ago
Mathematics is easy if you just brute force the problem
domain is not what is happening here
[–] pfdietz 2 days ago
Just low-hanging Fields Medal worthy results. Nothing to write home about, right?
[–] srdjanr 2 days ago
[–] bananaflag 2 days ago
The flagship case is AI itself, where we rely on benchmarks, not proofs (how could one prove "is good at seducing people").
Something that could have qualified as a "CS discovery" would have been, for example, a SAT or SMT solver that dwarfs in performance any existing one.
Something that could have qualified as a "physics discovery" would have been a new particle. Anyway, something that would come out of experimental data.
[–] RugnirViking 2 days ago
[–] drstewart 2 days ago