HN

Comments (74)

• Menu

  dvt
  I think Terry Tao is a great litmus test for AI zealotry (both pro- and anti-). Just in this thread, we have people twisting themselves into knots about how he "sold out" or "not doing math the right way" or whatever. To him, AI is a tool, like any other.From the interviews I've seen with Tao, he's not some AGI maniac, he says things like here's where we can use this tool, here's where it's less likely to be useful. There's a lot of hallucinations, so we need to double check stuff. Most of the stuff the AI produces is nonsense, but there's occasionally a diamond in the rough.A very tempered attitude, and likely what most sane people are experiencing when using AI.
• Menu

  YeGoblynQueenne
  I should really know better than to say something like that for a figure as revered as Terry Tao, but, he has taken OpenAI's money to shoot an advert for them [1] and, sorry but I can't believe he is entirely unbiased; or very unbiased for that._____________________[1] https://youtu.be/cdflu9ZXZGE?si=f1xi65r7kZM8s1JI
• Menu

  norir
  Terry Tao is a next level vibe coder: he inspires people to do his vibe coding for him. As someone with a background in advanced math, though never even close to Tao's level, I find myself skeptical about this type of mathematics. I don't personally find it beautiful and it feels like the line between the profound and the trivial (as in of minimal importance not difficulty) is blurry. One could argue for pure mathematics that is of no practical utility but is aesthetically beautiful, but I struggle to see the beauty in a gargantuan lean proof constructed by 100 different people. Perhaps this work will lead to deeper insight about the universe and the human condition, but I catch a whiff of problem solving for the sake of problem solving untethered from a deeper sense of purpose and meaning.
• arjie
  Woah, guys, the article is actually super cool. I almost didn't read the article because of the AI thing - I follow him on the microblog networks and I know he's pretty good at using LLMs and so on so that's not interesting. The unique stuff about him and gowers that it points out is there idea for massively parallelizable mathematics problem solving. It's definitely worth a read for how they got the first Polymath publication and afterwards for how they want to use LLMs et al. to do this:> He predicted that in the future, instead of working alone or in small teams of two or three, mathematicians might work on projects with hundreds of other people at a time. And when these collaborations were over, he said — in his modest, understated way — the results might be checked not by human referees but by computers.Fascinating stuff. My thought has always been that the AI will accelerate individuals and we'll get something like the economy for music or sports (the top few take almost all the revenue) but this may seem like an alternative pathway that might well develop (if only in Mathematics there) where AI systems drop the coordination cost to near zero by making checking cheap.So far, and I am not foolish enough to say forever, agents are great at operating in the space of checkables and it's hard to get uniqueness out of them (I haven't succeeded in getting a real laugh from Fable) but perhaps there's a whole class of problems that we can now solve by turning humans into the search units. I love it!
• Menu

  klmarks
  Quantamagazine is essentially Renaissance Fund, which is heavily invested in AI.This is a clever piece reminding people of Tao's pre-AI Lean efforts. Now, however, Tao and especially Gowers are receiving AI money and have AI positions so they are far from unbiased.Or maybe they have caught Feynman's "computer disease"? Either way, this is a hype piece.
• nylonstrung
  More accurate title would be "Terry Tao Became an Evangelist for Lean"
• Menu

  pvillano
  I really look forward to the day AI-driven algorithm design + formal verification becomes the norm for performance critical computing.A programmer translates a natural-language spec into a machine-readable spec, feeds it to an AI-assisted compiler, and out pops an implementation that's more optimized than any human could ever hope to write, along with a lean proof of its correctness.
• Menu

  ruilov
  the smartest people see AI as an incredible tool that enhances their productivity.
• vitriol83
  mathlib and lean are currently too cumbersome for many researchers to use in say algebraic geometry, but maybe more suitable for combinatorics where it has been applied recently.
• gosub100
  I have a tangent question: is there a formal language definition of mathematical grammar the same way there is for a programming language? If so, is it context sensitive or context free?I was daydreaming about how someone would model symbolic algebra in computer code, and naively thought it would be easy, but the more I thought about it, it seems to get exponentially (pun intended) more complicated.
• brcmthrowaway
  It seems Cameron Zwarich has also joined OpenAIIs there a Lean/OpenAI connection?
• cryo32
  And I thought it was cocaine.