PoudlardoLeanstral: Open-source agent for trustworthy coding and formal proof engineering
Lean 4 paper (2021): https://dl.acm.org/doi/10.1007/978-3-030-79876-5_37
Curious if anyone else had the same reaction as me
This model is specifically trained on this task and significantly[1] underperforms opus.
Opus costs about 6x more.
Which seems... totally worth it based on the task at hand.
[1]: based on the total spread of tested models
Agreed. The idea is nice and honorable. At the same time, if AI has been proving one thing, it's that quality usually reigns over control and trust (except for some sensitive sectors and applications). Of course it's less capital-intense, so makes sense for a comparably little EU startup to focus on that niche. Likely won't spin the top line needle much, though, for the reasons stated.
Ha, keep putting your prompts and workflows into cloud models. They are not okay with being a platform, they intend to cannibalize all businesses. Quality doesn't always reign over control and trust. Your data and original ideas are your edge and moat.
The same old speech that has been used throughout history. When cars were invented people complained to everyone that Ford intended to cannbolize all horse drawn carriages. When manufacturing was invented it cannibalized the work of all the sewing and knitting companies that had women making one item at a time. When Google was invented it cannabolized libraries, and encyclopedias, etc. etc.
Yet nobody wants a horse drawn carriage, nor to knit their own sweaters, nor go to the library to look things up in a physical encyclopedia.
Yet nobody wants a horse drawn carriage, nor to knit their own sweaters, nor go to the library to look things up in a physical encyclopedia.