sebzim4500

Yes my videos would suck whether I use AI or not I really don't understand what you are trying to say

>yes i know, but if you think you're no better than an LLM then why don't you put your personality into a system prompt and spare us the carbon footprint

There are still things I can do much better than AI, making videos just happens not to be one of them.

Plenty of people will watch it, souls don't exist.

Depends if you include a few decades of improvements in lean itself. Non-AI proof automation is much better than it was even a year ago and so some fiddly results can now be done with `by grind`.

Also don't discount the fact that people would learn how to do this kind of project, currently no one really knows how to decide what definitions work best, what should be reducible, what should be part of a public api and what should be local to a module, etc.

In general checking that the definitions are correct isn't that hard and assuming at least one of the lean kernels you verify with is correct (which tbf is an assumption, the implementations are based on each other so could have a common bug) that's all you need to verify.

In this case the statement is unusually complicated but still much much easier to verify than the proof itself.

It's nice to know that they didn't miss anything. The natural language proof is 10,000 pages and they have missed groups in the past.

This seems like a very good use of auto-formalization, because in the past mathematicians have incorrectly believed that they were finished with the classification only discover a missing class/sporadic group.

The original proof was a collaboration of ~100 mathematicians, if Tao is correct then we should expect to see more such collaborations in the future like we do in e.g. physics.

Well OpenAI has an opt-out setting to control whether they say they can train on your data, so it would be strange if they weren't training on at least some conversations with their models. Whether that is a meaningful contributor to the competency of their models (compared to e.g. just training on published papers) is something only frontier labs would be able to tell us.

They have released them, they are just also hiring mathematicians to clean them up in parallel.

If that's the goal then they can do it the other way round.

1. Pick random high quality maths papers that are outside of the training window 2. Convert them into a form which preserves the quality of the results but throws away the quality of the writing. For example, formalise them or keep only a high level summary of the proofs and throw away the introduction/conclusion 3. Generate full maths papers out of these summaries 4. Try to make the output maths papers be as similar as possible to the input papers.

You can see this as similar to training an auto-encoder, and I don't see any real downside to doing this over training on these corrected papers. Yes, the individual results would be less significant but you can't exactly mass produce training data by publishing papers and hoping someone fixes it.

Maybe, but I don't see why it would be better than selecting random maths papers

How does any of this benefit OpenAI? They already got the headlines, it's not like its going to be front page news when the mathematical community actually understands the results that have already been claimed.

It's not locally hosted, as they say they will be accessing the same models but through a controlled system rather than on their own accounts

You forgot to specify that f(n) approaches 1 so that is an easy challenge