Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- 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.
by gosub100 - the smartest people see AI as an incredible tool that enhances their productivity.by ruilov
- 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.
_____________________
- More accurate title would be "Terry Tao Became an Evangelist for Lean"by nylonstrung
- 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.
by pvillano - I guess fandom is just in Terry's DNA: http://shanghikid.50megs.com/Otakudom/ContReal/contReal.htmby spondyl
- 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!
by arjie - When I was in college, I posted a question on math.se about possibility of universal gates like NOR and NAND in multi-level logic. Someone found it interesting and posted it on the mathoverflow in more mathy language . To my surprise, Terry wrote an answer to that question. I still don't get it but I was flexing the whole month.
Terry also took time to respond to comments I posted on his blog and on his google wave posts (I am old). Most of them were incredibly stupid but he took time to respond. Imagine a field medalist responding to a wannabe kid living somewhere in India.
Some of his real analysis notes were published in India that were cheaply available. I learnt about open/close set and convergence/cauchy series from it. I never thought I'd enjoy reading pure mathematics. Another mathematician I found very readable Daniel Spielman (I think it was his notes on smooth analysis). I once picked a book by William Tutte from the library! Never seen a book that was harder to read.
I don't know what the point of my post is.
by dilawar