> Although the current generation of models is trained to complete tasks rather than to enrich our understanding, and today’s AI companies are misaligned with the goals of the mathematical community, I hope that with time we’ll find ways to use these tools in harmony with human research.
while citing "A Severe Misalignment of AI in Mathematics" [1], which condemns exactly the thing he is doing himself: Mindlessly producing theorems without a corresponding human understanding of the underlying proofs.
Perhaps you and I read this document differently. This is not a “famous problem”, I am not a “major AI company”, and I am genuinely interested in increasing mathematical understanding. To the last point, here is a comment from a mathematician who co-authored the paper that my proof is largely built upon: <a href="https://news.ycombinator.com/item?id=49761718">https://news.ycombinator.com/item?id=49761718
The happy case here is that my obtuse proof leads to a concise and illuminating mathematical proof, which is exactly my hope for the endeavour. I think this could then be a positive example of AI/human and amateur/professional collaboration.
What would a positive example look like to you? What do you think the manifesto argues for?
Okay, at least the comment from the mathematician sounds positive.
Positive example: Someone is 1) independently interested in a particular conjecture, 2) he lets an LLM prove and explain it, 3) he ends up fully understanding the LLM proof and is then able to phrase it in his own words.
cubefox · · focus · HN ↗
> Although the current generation of models is trained to complete tasks rather than to enrich our understanding, and today’s AI companies are misaligned with the goals of the mathematical community, I hope that with time we’ll find ways to use these tools in harmony with human research.
while citing "A Severe Misalignment of AI in Mathematics" [1], which condemns exactly the thing he is doing himself: Mindlessly producing theorems without a corresponding human understanding of the underlying proofs.
1: <a href="https://mathandai.org/" rel="nofollow">https://mathandai.org/
danabramov · · focus · HN ↗
The happy case here is that my obtuse proof leads to a concise and illuminating mathematical proof, which is exactly my hope for the endeavour. I think this could then be a positive example of AI/human and amateur/professional collaboration.
What would a positive example look like to you? What do you think the manifesto argues for?
cubefox · · focus · HN ↗
Positive example: Someone is 1) independently interested in a particular conjecture, 2) he lets an LLM prove and explain it, 3) he ends up fully understanding the LLM proof and is then able to phrase it in his own words.