Machine-Assisted Proof [pdf]

Post by [deleted] » Sat, Dec 28, 2024, 11:02 AM UTC

simplemathmind wrote: post #21

generationP wrote: post #18

Earlier quoted context omitted.

Right, and the paper you didn't read contains a lot more than that.

I apologize in that case, can you give a brief summary of what is the most important point of that pdf?, I don't know why but my gut feeling is to refuse to read something just based on people reputation. I know that Tao is a very bright mathematician but I also think that he doesn't know much about computer science or computer languages (my evidence is very slim here: once I noted that Tao was very happy with a very…

Post by brap » Sat, Dec 28, 2024, 11:14 AM UTC

vouaobrasil wrote: post #29

I think his comparison to previous machine-assistance is misleading. In previous cases, the use of machines was never creative, whereas now AI has the ability to suggest creative lines. In the short-term, this sounds exciting. But I also think it reduces the beauty of math because it is mechanizing it into a production line for truth, and reduces the emphasis on the human experience in the search for truth. The same…

Post by vouaobrasil » Sat, Dec 28, 2024, 11:19 AM UTC

brap wrote: post #33

vouaobrasil wrote: post #29

I think his comparison to previous machine-assistance is misleading. In previous cases, the use of machines was never creative, whereas now AI has the ability to suggest creative lines. In the short-term, this sounds exciting. But I also think it reduces the beauty of math because it is mechanizing it into a production line for truth, and reduces the emphasis on the human experience in the search for truth. The same…

Human chess players are still incredibly valuable because we want to see what humans are capable of. For the same reason athletes are valuable even though a car can outrun them. With mathematicians, and others working in intelligence-intensive tasks (most of us here probably), I’m not sure what the value would be post-AGI.

Post by throwaway127467 » Sat, Dec 28, 2024, 11:31 AM UTC

jiggawatts wrote: post #34

kartwna wrote: post #10

"I have found it works surprisingly well for writing mathematical LaTeX, as well as formalizing in Lean; indeed, it assisted in writing this very article by suggesting several sentences as I was writing, many of which I retained or lightly edited for the final version. While the quality of its suggestions is highly variable, it can sometimes display an uncanny level of simulated understanding of the intent of the tex…

Something I've noted about all advanced tools is that the inept fear them, the capable use them, and the elite embrace them wholeheartedly. Everything from IDEs to Google search gets the same treatment. I remember a colleague watching me edit code exclaiming that I was "Cheating!" because I had syntax highlighting and tab-completion. Another coworker who had just failed to get answers after searching for "My PC crash…

Post by williamcotton » Sat, Dec 28, 2024, 11:38 AM UTC

vouaobrasil wrote: post #35

brap wrote: post #33

Earlier quoted context omitted.

Human chess players are still incredibly valuable because we want to see what humans are capable of. For the same reason athletes are valuable even though a car can outrun them. With mathematicians, and others working in intelligence-intensive tasks (most of us here probably), I’m not sure what the value would be post-AGI.

The point is that even with mathematics and programming, there is an underlying community aspect that cannot be ignored, but is hidden under layers of utility. For example, even in programming, people getting together to code, collaborating, and sharing their projects is a small but significant drop in people creating a community. With mathematics, the sharing of ideas and slaving over the proof of a theorem brings m…