The problem of the proof was that we knew that FCT was true, but we had no idea why. A good/elegant proof teaches us something new about how that problem is related to other problems. It isn't just about getting a true/false answer to the conjecture.
omnicognate 1 hours ago [-]
Indeed, and the computer aided proof discouraged research into the insightful proof a lot of mathematicians think is probably out there to find. "Proved but not insightfully" is a problem status some mathematicians are starting to think of as closer to "open" than "closed", which is a good thing IMO. (I am not a mathematician, though)
whatshisface 33 minutes ago [-]
Maybe the new heuristic auto tactics will lower the cost of finding the human proof of the four color theorem enough to be affordable in the current environment.
utopcell 24 minutes ago [-]
> "The problem of the proof was that we knew that FCT was true"
Citation needed.
fhdkweig 17 minutes ago [-]
That was terrible phrasing. I meant "The problem with the proof was that although it showed that FCT was true, the proof did not explain why".
aaron695 8 minutes ago [-]
[dead]
jjtheblunt 40 minutes ago [-]
the title made me think of a much older machine that was used for calculating
> I would like to conclude by telling a cautionary tale. Let us try and place the Antikythera Mechanism within the global context of ancient Greek thought. Firstly came the astronomers observing the motions of the heavenly bodies and collecting data. Secondly came the mathematicians inventing mathematical notation to describe the motions and fit the data. Thirdly came the technicians making mechanical models to simulate those mathematical constructions, like the Antikythera Mechanism. Fourthly came generations of students who learned their astronomy from these machines. Fifthly came scientists whose imagination had been so blinkered by generations of such learning that they actually believed that this was how the heavens worked. Sixthly came the authorities who insisted upon the received dogma. And so the human race was fooled into accepting the Ptolemaic system for a thousand years.
> Today we are in danger of making the same mistake over computers. Our present generation is able to view them with an appropriate skepticism when necessary. But our children's children may be brought up within a society dominated by computers, that they may actually believe this is how our brains work. We do not want the human race to be fooled again for another thousand years.
I think a lot of great ideas like tree-width were developed in hope of simplifying the proof.
layer8 1 hours ago [-]
I didn’t know we had invented time machines yet. ;)
evekayser 2 hours ago [-]
I think the same happens now with AI generating code. Nobody will read every line. that's part of the process from now on.
curt15 1 hours ago [-]
The human who commits a bad change still takes the fall though. Automation doesn't absolve accountability.
Insanity 1 hours ago [-]
But people think it does, and it’s annoying. The past months I’ve often found mistakes and then heard the response along the lines of “oh Claude wrote that”.
It’s used as an excuse, and then the conversation just moves on. I don’t see a lot of accountability being taken. If anything, senior leadership sees it as a sign of adoption and accepts a certain level of risk.
godwinson__4-8 16 minutes ago [-]
What is "taking accountability" supposed to look like in this case?
As an aside, trying to enforce some cultural more without the backing of senior leadership is a waste of time. You should probably follow your colleagues example and get a better return on your time with Claude and stop caring. If you are the only one at your company who cares and you aren't the largest shareholder I have to ask under what economic theory you are operating. Unless you work for a charity or something you should probably either find a new job or stop complaining about the relative luxury of being handed a fistful of money just to be able to say "Claude wrote that".
Apparently no one at your company cares, so why do you?
Rendered at 21:56:46 GMT+0000 (Coordinated Universal Time) with Vercel.
Citation needed.
https://en.wikipedia.org/wiki/Antikythera_mechanism
> Today we are in danger of making the same mistake over computers. Our present generation is able to view them with an appropriate skepticism when necessary. But our children's children may be brought up within a society dominated by computers, that they may actually believe this is how our brains work. We do not want the human race to be fooled again for another thousand years.
-- E.C. Zeeman, Gears from the Greeks, January 1986, http://zakuski.utsa.edu/~gokhman/ecz/gears_from_the_greeks.p... (https://web.archive.org/web/20250502052226/http://zakuski.ut...)
It’s used as an excuse, and then the conversation just moves on. I don’t see a lot of accountability being taken. If anything, senior leadership sees it as a sign of adoption and accepts a certain level of risk.
As an aside, trying to enforce some cultural more without the backing of senior leadership is a waste of time. You should probably follow your colleagues example and get a better return on your time with Claude and stop caring. If you are the only one at your company who cares and you aren't the largest shareholder I have to ask under what economic theory you are operating. Unless you work for a charity or something you should probably either find a new job or stop complaining about the relative luxury of being handed a fistful of money just to be able to say "Claude wrote that".
Apparently no one at your company cares, so why do you?