The whole point was for the formalization to be clean enough so it could be reused in other parts of mathematics as I understand it. 13M lines of AI slop which have never been checked do not sound like what the original goal for such a formalization was. Also Claude didnt prove anything it just translated an already existing proof by Wiles into Lean, so it didn't actually contribute anything other than "Guys we did this thing, look how great our model is!". We never questioned that a printer can print faster than a human can write, but we dont let printers write novels.
Its 27B not 37B and having just 27B in total and 3T and like 30B active of those is still totally different. A 120B with 5B active is still much slower than a proper 5B. Just like the new Ling 3.0 Tiny with 8B and 1B active only gets around 120tk/s compared to 250tk/s which a real 1B one gets on my hardware.
At one point there were specific -Coder release of Qwen e.g. 2.5 but they dropped that, still wondering how much better 3.6-Coder or 3.8-Coder would be when they ignore everything else
Here you have shown yourself that progress slows down and doesnt speed up. 8.9/0.35 = ~25x more performance in 10 years from 2006 to 2016. 104.8/8.9 = ~12x more performance in 10 years from 2016 to 2026. Growth has dropped 50%.
If you could render fully in OpenCL and output it via another device it would probably work. But they dont have ROPS so they cant do traditional video rendering. Even something like Blender where you would use it for calculations and not for display/video doesnt work without software emulating hardware features related to textures.
Old datacenter GPUs could game, but new ones can only do OpenCL/CUDA/ROCm etc. and have no display out. Im using an MI50 right now and I would wish newer datacenter cards could also be used for everything like them.
The wording wasnt very good I ment compared to programming or math the amount of logic and reasoning is small (Research level math hardly compares to writing a book in raw reasoning and logic). And I thing the smaller models have enough "intelligence" to write coherent with logical world building, but only the big models can truly do hard math and programming work
Do people really use 100B+ models for writing? I am no writer but to me it seems like writing is one of the easiest tasks with barely any logic or reasoning and as long as its not longer than a handful of pages I expect even 8B models to perform great.
I think model training is pretty hard to do efficiently on a vastly distributed network. If the model cant fit into the VRAM of the node your performance becomes so bad its useless, so a distributed model could only be properly trained if the size of the model doesnt exceed the majority of the nodes VRAM sizes. Maybe there is a different way of doing training but this would be the only way I can see. And it would still be much worse than just using a big datacenter where everything is fully interconnected. BOINC projects work great because its usually just a lot of small compute and memory required so every old desktop and laptop can contribute. Training a model which can compete and is not tiny requires neither low compute or low memory amount. BOINC tasks take minutes usually or sometimes hours but not weeks or months like training a model from scratch. But something like 7B or lower could maybe be trained like this. Im not sure but I think someone is already working on something like this but I dont remember the name of the project.