Viewing profile — 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 fo…

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 y…

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 alr…

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,…

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 harde…

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 f…

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 powerf…

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 for…

The field is fairly new to me. I'm originally from computer algebra, and somehow struggling into the field of ATP. The most interesting papers to me personally are the following th…

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 a…

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 d…

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…

How on earth could you evaluate the scaling path with too little information. That's my point. You can't possibly know that a technology can solve a given kind of problem if it can…

I think maybe I didn't make myself quite clear here. There are already algorithms which can solve advanced mathematical problems 100% reliably (prove theorems). There are even algo…

There are certainly efforts along the lines of what you suggest. There are problems though. The number of backtracks is 10^k where k is not 2, or 3, or 4..... Another issue is that…

I've tested GPT-4 on this and it can be induced to give up on certain lines of argument after recognising they aren't leading anywhere and to try something else. But it would requi…

I feel very comfortable saying, as a mathematician, that the ability to solve grade school maths problems would not be at all a predictor of ability to solve real mathematical prob…

The tendency to begin summarising is very annoying. I'd assumed it was because of limited attention span of human raters who rated summarised or shorter outputs more highly. And I'…

One mildly good thing to say about Loeb is that he spoke out very harshly about the quantum woo that the UAP "whistleblower" David Grusch invoked to potentially explain how aliens …

The new 4x4 matrix multiplication over F_2 has practical applications as many matrix operations over F_2 can be reduced to matrix multiplication. For anyone looking for the algorit…

Technically it all runs in 500kb I think (not sure if this includes DOS). And this was intentional because the guys had in mind what people would typically have available. However …