So far we haven't seen much of that consolidation. And a lot of people are using trailing edge models just fine already. > [...] but the level of quality that

So far we haven't seen much of that consolidation. And a lot of people are using trailing edge models just fine already. > [...] but the level of quality that is considered essential for work will always stay pinned at "near-frontier". Why? When we'll finally all write our software in Lean and prove it correct and prove it fast, it won't matter that a slightly more clever model could have found a slightly nicer proof or whatever. Just like today people happily use Python for many programs, even though rewriting in C might give you a performance boost. Good enough is often good enough.