A few days ago I read a fascinating article in New York magazine: Inside the AI Factory, which explained how the very large business of hiring humans to do tasks that generate training data for AI works. One reaction I had to this was “at least this means math is safe from AI, nobody is going to pay mathematicians to generate this sort of training data.” Yesterday though I ran across this tweet from Kevin Buzzard, which advertises work (see this link) that seems to be of this kind.
A company called Prolific is advertising work paying 20-25 pounds/hour doing tasks in Lean 3. This company is in exactly the business described in the NY mag articles, hiring people to do tasks as part of “studies”, which often are generating AI training data.
One unusual thing about this whole industry is that if you sign up for this work you often have no idea who your employer really is, or what your work will be used for, and you sign a non-disclosure agreement to not discuss what you do. In this case, a few things can be gleaned from discussions on the Lean Zulip server:
- “it’s 40 dollars/hr now actually”
- “I think everyone signed a consent form preventing them from disclosing any problems or even their participation.”
- One problem was formalizing a proof of sin(x)=1 implies x=pi/2 (mod 2pi).
- A representative of the company writes: “Some of our biggest partners are keen to work with Lean users because of its applicability as a theorem prover. They plan to launch numerous studies that require participants to have either a working or expert knowledge of Lean 3.” By “biggest partners”, presumably this is Microsoft/Google or something, not some small publishing organization.
If anyone knows anything about what’s up with this incipient possible math AI factory, please let us know. On the more general issues of math and AI, I’d rather not host a discussion here, partly because I’m pretty ignorant and not very interested in spending time changing that. The situation in mathematics is complicated, but as far as fundamental physics goes, theorem-proving is irrelevant, and applying “big data”/machine-learning/AI techniques to generate more meaningless calculations in a field drowning in them is pretty obviously unhelpful.
For a much better place to read about what is happening in this area, there’s an article in today’s New York Times by Siobhan Roberts: A.I. Is Coming for Mathematics, Too. At Silicon Reckoner, Michael Harris is in the middle of a series of posts about this past month’s workshop on “AI to Assist Mathematical Reasoning.”
Thanks for the NYT-link! I find Williamson’s remark: “a simple neural net that predicted “a quantity in mathematics that I cared deeply about,” he said in an interview, and it did so “ridiculously accurately.” Dr. Williamson tried hard to understand why — that would be the makings of a theorem — but could not. Neither could anybody” very interesting. What is that “quantity”? And was that just one incident, or one among others?
Linking to a tweet without quoting anything from it is now basically useless, since Twitter is getting more and more broken. Just saying….
Just want to +1 what David Roberts said. I can’t currently read that tweet by Kevin Buzzard (“Something went wrong. Try reloading.”). Who knows what set of people will be able to read it on any given day in the future…. So it’s definitely sensible practice to quote the text of the tweet as well as linking to it.
David Roberts/James Martin,
I’ll add the relevant link to the Prolific site that was in the Buzzard tweet.
As for Twitter problems, the one James Martin’s message refers to I also had, fixed by deleting cookies (clear info stored in browser).
Elon Musk made Twitter not viewable without logging in.
@Thomas try https://doi.org/10.1038/s41586-021-04086-x though the Williamson quote is lacking in detail and context, so I don’t know if the same situation or a different one.
Haven’t heard from anyone who knows what might be going on here. My current best speculation: this is Microsoft, part of work on future versions of the Math Solver tool, see https://math.microsoft.com
Lean originates at Microsoft, which would explain why they are focused on that. Having a large data set of formalized solutions to math problems created by humans might be something useful for developing an AI system capable of doing this.
@Thomas:
I provide details below. In the future I can imagine many situations where neural networks are making accurate predictions, however the “why” is missing. I am a professional mathematician, and I stared for several days at the actual matrices of the model, without any insight whatsoever. This was a real lesson for me.
Now to technical details (I will assume some familiarity with the Nature paper linked by David Robers): One of the first things we tried to do is predict the coefficient of q in a Kazhdan-Lusztig basis element from a piece of the Bruhat graph. (The piece we were concerned is displayed in Figure 5-c: “First-order neighbours and diamonds”.) There is no known theoretical result that such a prediction is possible. We were using a small graph neural network, and it was getting >99% accuracy. (I am operating from memory now, but I seem to recall that Alex Davies and Lars Buesing at DeepMind used distillation techniques to reduce the network size to a single 5×12 matrix + global max pooling layer. Even this network which is tiny compared to typical neural networks was not interpretable.)
@Geordie: Many thanks!
@Peter Woit
This is getting into my area. I would speculate that curating a large enough corpus of pairs of machine proofs in LEAN with human language equivalents will lead to LLM’s capable of generating machine proofs in LEAN when given human language theorems. That’s probably what is going on here.