How should I read this?

There is some illuminatingchatter on the lean Zulip about this. Including the authors.

I am on an infinite ad loop with the link. Is it just me?

It would have to be faster in GPU hardware and they would have to be able to budget for it, given how expensive GPUs are at scale.

I recall that there is some research into sparsifying neural network weights as well. This sort of speed up might be cheaper.

Maxwell’s equations were perfectly sufficient for radios.

I think I recognise Indian English there. “I’d love a pointer” is Indian corporate-speak.

I must note that it would be harder to check the correctness of definitions and theorems in such an autoformalisation than review the pen and paper version in a conference.

This is not to say that they can’t get better at this stuff, but the bigger the formalisation effort, the less one should trust an AI with the definitions and theorem statements. And even after ensuring correctness, such a formalisation would be devoid of all the uses one could put it to.

In general there is a wide gap between what ML researchers achieve in experiments and how well it works in practice. In addition, there is a deployment gap. In our equational theories project we explicitly noted that modern AI was extremely underwhelming.

Yes. This was discussed in the lean Zulip. I don’t take it too seriously for the following reason. This tool was provided a very fine grained blueprint. I can imagine that for the typical SODA paper, even with all the prerequisite material existing in some library, it would be a 1000 pages.

I am inclined to believe that AI tools will have the same effect on formal proofs. They might take users to intractable proof states and give up when used or modify definitions incorrectly to get proofs accepted.