If they aren't "smart enough" to know if it work they most likely are also unable to verify if the Lean formalization is indeed the one that matches the problem they were trying to solve.
Verifying that every step in a (potentially long) proof is sound can of course be much, much harder than verifying that a definition is correct. That's kind of the whole point.
That's not what the parent comment meant. They meant checking the Lean-language definitions actually match the mathematical English ones, and that the Lean theorems match the ones in the paper. If that's true then you don't actually need to check the proofs. But you absolutely need to check the definitions, and you can't really do that without sufficient mathematical maturity.
Yes, and the child comment’s point is that formalizing the problem is likely easier than having the LLM verify that each step of a long deduction is correct, which is why Lean might be helpful.
But both of you are ignoring the parent comment! Actually you're ignoring the context of the thread.
Originally someone said "I wish I was math smart to know if [this vibe-mathematics proof] worked or not." They did NOT say "I'd like to check but I am too lazy." Suggesting "ask it to formalize it in Lean" is useless if you're not mathematically mature enough to understand the proof, since that means you're not mathematically mature enough to understand how to formalize the problem.
Then "likely easier" is a moot point. A Lean program you're not knowledgeable enough to sanity-check is precisely as useless as a math proof you're not knowledgeable enough to read.
That's great if it works. But it's way harder to produce a formal proof. So my expectation is that this will fail for most difficult problems, even when the non-formal proof is correct.
I can't find it now but I once read that people who report the "paradoxical reaction" to stimulants have a significantly better outcome from stimulant medications, and both those values seem to have higher heritability than ADHD as a whole, possibly even linked to a single gene.
Following the bottle-cap madness, I don't think any current data shows the actual issue was resolved. Even worse, the effect on marine life is still not measured, and afaik reduction of harm was the primary goal. Instead of brutally high fines on fishing net waste, we got bottle-cap madness.
We have so much experience with scientific method, yet these massive decisions are adhoc, that's how the whole world works. We never tested what would happen by allowing mass production of plastic, or phones, or whatever, so these antipatches are going by the "feels" as well, with no individual taking responsibility for failures.
There is monitoring of beach pollution but data publication is typically delayed, like, we know it went down by 30% from 2015-2016 to 2020-2021, we will have data on a regulation that went into force in late 2024 only in a few years.
A bit off topic, but I recently had a drink that didn't have the attached bottle cap while travelling abroad, and my god, was it a minor annoyance to have to hold the bottle cap in my hand while drinking. I also almost dropped it because I expected it to stay attached. Funny how fast we adapt.
haha, all of a sudden I see a tab "waifu pillow" on Amazon, and think I have a split personality that runs searches in between consciousness shifts, and then I come back to a funny message.
That's fair, but "what about animals" is to "we should not torture human brain organoids" as "what about plants" is to "we should not torture animals".
I am suffering substantially more psychic damage from being forced to watch videos of pig euthanasia at meathouses than any pig has ever suffered from being euthanized at one of those meathouses, because I have 10x the neurons as a pig and therefore e^10 more capacity for pain.
I had a similar feeling trying to calculate some combinatorial structures. At some point the LLM made a connection to extremal combinatorics and calculated tighter bounds and got me to the solution faster.
Felt flashbacks of playing chess against humans online as a teen by copying moves from a chess engine.
Libraries create boundaries, which are in most cases arbitrary, that then limit the way you can interact with code, creating more boilerplate to get what you want from a library.
Abstractions are the source of bloat. Without abstractions you can always reduce bloat, or you can reduce bloat in your glue, but you can't reduce glue.
It takes discipline to NOT create arbitrary function signatures and short-lived intermediate data structures or type definitions. This is the beginning of boilerplate.
So many advances in removing boilerplate are realizing your 5 function calls and 10 intermediate data structures or type definitions, essentially compute a thing that you can do with 0 function calls and 0 custom datatypes and less lines of code.
The abstraction hides how simple the thing you want is.
Problem is that all open source code looks like the bloat described above, so LLMs have no idea how to actually write code that is without boilerplate. The only place where I've seen it work is in shaders, which are usually written to avoid common pitfalls of abstraction.
LLMs are incapable of writing a big program in 1 function and 1 file, that does what you want. Splitting the program into functions or even multiple files, is a step you do after a lot of time, yet all open source looks nothing like that.
> Abstractions are the source of bloat. Without abstractions you can always reduce bloat, or you can reduce bloat in your glue, but you can't reduce glue.
Yep, people not understanding the value of abstraction is exactly why LLM coded apps are going to be a shit show. You could use them to come up with better abstractions, but most will not.
White colar work is just a lucky place to be, 99% of it is completely made up, there's people doing nothing, and people doing work of 10 people, does not matter, the work itself has no impact on anything.
A nice way to realize why this AI wave hasn't produced massive economy growth, it is mostly touching parts of economy which are parasitic and can't really create growth.
reply