wbhart

I have not been working on formalization but theorem proving, so I can't confidently answer some of those questions.

However, I recognise that there is not so much training data for LLMs wanting to use the Lean language. Moreover, you are really teaching it how to apply "Lean tactics", which may or may not be related to what mathematicians do in standard texts on which LLMs have trained. Finally, the foundations are different: dependent type theory, instead of the set theory that mathematicians use.

My own personal perspective is that esoteric formal languages serve a purpose, but not this one. Most mathematicians have not been hot on the idea (with a handful of famous exceptions). But the idea seems to have gained a lot of traction anyway.

I'd personally like to see more money put into informal symbolic theorem proving tools which can very rapidly find a solution as close to natural language and the usual foundations as possible. But funding seems to be a huge issue. Academia has been bled dry, and no one has an appetite for huge multi-year projects of that kind.

Lean is an interactive prover, not an automated prover. Last year a lot of human effort was required to formalise the problems in Lean before the machines could get to work. This year you get natural language input and output, and much faster.

The advantage of Lean is that the system checks the solutions, so hallucination is impossible. Of course, one still relies on the problems and solutions being translated to natural language correctly.

Some people prefer difficult to read formally checked solutions over informal but readable solutions. The two approaches are just solving different problems.

But there is another important reason to want to do this reliably in natural language: you can't use Lean for other domains (with a few limited exceptions). They want to train their RL pipelines for general intelligence and make them reliable for long horizon problems. If a tool is needed as a crutch, then it more or less demonstrates that LLMs will not be enough in any domain, and we'll have to wait for traditional AI to catch up for every domain.

1. Correct

2. Correct, however you can use Waksman as a basecase and always beat Strassen (though it is not asymptotically better of course).

5. Possible, but even so, there is already an algorithm that will work with 46 real multiplications (and some divisions by 2). The real numbers are commutative and admit division by 2.

Z_2 has characteristic 2, not 0.

As already noted in a post by fdej further down, Waksman's algorithm from 1970, which works over the complex numbers, requires only 46 multiplications (and I guess, divisions by 2, which may or may not be relevant depending on your actual ring).

There's even an Open Source implementation of Waksman's in Flint, the package fdej maintains.

I've been using MartyPC for a few years and except for emulating glitches in hardware which depend on the manufacturer, date of manufacture or even temperature, it is getting harder to find cycle accurate tricks that MartyPC can't emulate perfectly (believe me, we've been trying).

The whole thing is a marvel of software engineering!

What is remarkable is that the author (GloriousCow) doesn't complain that people are ripping off his code and ideas, but that more people haven't used his learnings to create other cycle accurate emulators for the PC.

This blog article is written in a very engaging way. It seems to be more or less a masterclass on how to keep someone's attention, although there is no meta-story making you wait for the big fulfillment at the end.

I think it is the short, punchy sections with plenty of visuals and the fact that you are telling a story the whole way through, which has a natural flow, each experiment you describe, leading to the next.

This is an interesting article, but the absence of simple examples of theories and their toposes and invariants made it seem a little abstract. Surely if the technique is so powerful, there ought to be easy examples of it aplenty.

I doubt that he was intending a burn here. He's not talking about user interface issues or the like.

He's most probably, I would assume, talking about the well-known issue that formalisation tools require knowledge that a standard mathematician doesn't possess, such as the names of all the Lean tactics, how to locate the right theorem to use in mathlib (the Lean library), the necessity to write mathematics in a very formal language which is based on dependent type theory rather than based on sets (which is what most mathematicians are used to), etc.

Moreover, formalised mathematics does not work with natural language (and perhaps can't), and it will not accept informal or intuitive arguments. There are a lot of very fiddly things that have to be attended to. One can't assume that the reader is a skilled mathematicians who can easily fill in trivial details, as when writing a maths paper for expert readers.

But the Lean people are acutely aware of all of this. In my opinion he's not so much offering them much needed criticism so much as acknowledging one of the known barriers to mathematicians from outside the formalisation community getting into formalisation.

This is a major point of the article, that real, serious mathematicians have broken through that barrier recently, and it's not the first time. So things have improved enough to show that it is possible for seriously committed mathematicians to do this, even famous ones!

Yes, there are various approaches like tree-of-thought. They don't fundamentally solve the problem because there are just too many paths to explore and inference is just too slow and too expensive to explore 10,000 or 100,000 paths just for basic problems that no one wanted to solve anyway.

The problem with solving such problems with LLMs is that if the solution to the problem is unlike problems seen in training, the LLM will almost every time take the wrong path and very likely won't even think of the right path at all.

The AI really does need to understand why the paths it tried failed in order to get insight into what might work. That's how humans work (well, one of many techniques we use). And despite what people think, LLMs really don't understand what they are doing. That's relatively easy to demonstrate if you get an LLM off distribution. They will double down on obviously erroneous illogic, rather than learn from the entirely new situation.

Sure, but people have already applied deep learning techniques to theorem proving. There are some impressive results (which the press doesn't seem at all interested in because it doesn't have ChatGPT in the title).

It's really harder than one might imagine to develop a system which is good at higher order logic, premise selection, backtracking, algebraic manipulation, arithmetic, conjecturing, pattern recognition, visual modeling, has a good mathematical knowledge, is autonomous and fast enough to be useful.

For my money, it isn't just a matter of fitting a few existing jigsaw pieces together in some new combination. Some of the pieces don't exist yet.

People have done experiments trying to get GPT-4 to come up with viable conjectures. So far it does such a woefully bad job that it isn't worth even trying.

Unfortunately there are rather a lot of issues which are difficult to describe concisely, so here is probably not the best place.

Primary amongst them is the fact that an LLM would be a horribly inefficient way to do this. There are much, much better ways, which have been tried, with limited success.