Hacker News

points by sevenzero 2 days ago | 0 comments

If everything of this can be represented in Lean, with enough compute, they are low hanging fruits, yes

So maybe everything is now low hanging fruit, with your definition.

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.

[–] hardbass 2 days ago

If everything can be represented in a Turing computer or a Fourier Series, does it make it trivial? Are you sure you know the computability power of these representations?

[–] saikia81 2 days ago

Mathematics is easy if you just brute force the problem domain is not what is happening here