> we urgently need to come up with good ways of explaining the value of having a large pool of human mathematical experts, even if it is no longer part of their role to find new proofs of theorems.
This is the main issue, and while I fully agree with that value sentiment, the referenced letter failed to provide convincing arguments for why mathematicians should widely receive funding for merely understanding things, and how competition for postdoc and tenure positions would work.
I’d say the deciding factor is that it has bugs where both fixing and not fixing them can have a negative impact. If there were no known bugs and there was no harm in using it, I’d probably just leave it there and not disturb anything, given that its use is so widespread, and instead merely note in the documentation that its purpose has become obsolete.
It reduces n items to one item, recursively. The items don’t have to have the same type. Arguably accumulate is a more fitting name. I think of “reduce” as in cooking, boiling a volume of stuff down to some essence.
Physics/cosmology-related HN submissions tend to have poor comment quality, so this being upvoted to the front page isn’t too surprising, unfortunately.
When you want to change the resulting program (“formal logic”), you generally don’t change the prompt and regenerate everything (like you would do with source code). Instead, you provide new natural-language instructions to have the LLM perform the change. This means that you don’t have a reproducible specification on the level where you are describing the specification. Therefore the thing that you are maintaining is not a natural-language artifact, it’s effectively still the formal description (program code).
And that’s why the parent comment is saying that we need people that understand the thing that is being maintained, i.e. the program code, which is the source of truth about what is being maintained.
> we need people that understand the thing that is being maintained
We do for a lot of software today, but not all of it. I think in a year we'll need them for less, but I'm not sure how much less.
This claim isn't supported or justified by talking about natural language versus formal language. For the last 50 years or so the people shaping a lot of software in the most important ways are often using only natural language.
The product manager doesn't understand the code today. They write PRDs and Jira tickets and comments in Slack, and software comes out. They have people test the software, report bugs, more software comes out. Eventually they decide its close enough to their vision to ship, without ever understanding or looking at any of the code. They can do that with human programmers or agent programmers. The former holds up better in larger systems, but I don't see any evidence for the proposition that this is due to the limits of natural language.
Developers are making a lot of important decisions in detail that the product manager has little understanding of, and these often lie exactly in the disparity between natural and formal language. What the product manager writes isn’t a full specification of the system.
This is the main issue, and while I fully agree with that value sentiment, the referenced letter failed to provide convincing arguments for why mathematicians should widely receive funding for merely understanding things, and how competition for postdoc and tenure positions would work.
reply