If the Lean initial-problem-setup/statements/assumptions/etc. aren't correct then the proof is meaningless. Lean does not know what it is that it is proving i.e. it does not have any semantic understanding but only executes formal logic.
It means "developing an overall way of looking at and approaching things strategically, which allows one to understand and act almost intuitively and effortlessly, under all circumstances and scales."
With the above approach, when you gain expertise in any one art with deliberate practice (body and mind), something changes and becomes part of your body/psyche/mind (i.e the holistic you) which if you internalize and consciously redirect to other arts will help you master them too effortlessly and intuitively.
Musashi embodied the above by also becoming a self-taught exceptional painter/calligrapher/sculptor.
If one reads the book with the above in mind then there is much to gain and apply in one's own life.
> Public posts on the internet are acceptable (to me).
Everybody needs to rethink this again.
Before LLMs the barrier to entry for building a character profile based on your various public posts was quite high. Remember "Psychographics" (https://en.wikipedia.org/wiki/Psychographics) and the infamous "Cambridge Analytica"?
Earlier it involved data mining, data cleaning, structuring data, building models, running algorithms and then evaluating the results for semantic information. Now it is straight to unfiltered semantic inference using a single sentence prompt (eg. point it to your HN profile and see what you get).
I actually did this on my HN profile and found it troubling. There were many unwarranted/hallucinated inferences due to the fact that it requires "commonsense reasoning" (https://en.wikipedia.org/wiki/Commonsense_reasoning), understanding human motivations and behaviour, context, assumptions, societal knowledge etc. which LLMs are bad at.
PS: You can cut-and-paste the above paras into a LLM prompt and ask it to elaborate for further details. The system itself will explain to you the problems/deficiencies which are quite scary.
Shenanigans is an inaccurate word; it implies underhanded behavior that's hidden / concealed. I think "to act so aggressively" is more balanced.
Here's my answer: If you think we're getting to AGI in the next 9 months, then you believe, with all your heart, that these problems will fall soon. However, there's an ocean to boil in terms of what you could point your limited clusters at. In the meantime, the market is desperate for any sign your company might be first to AGI. Therefore, news of tractability with current models might focus an organization intensely - internally they have a huge leg up on the public, and therefore it's minimal compute to check - and if they are successful, they get approximately $50 million of free PR, likely adding 10-20% to their valuation.
Likewise someone like Tristan is fighting for his (metaphorical) life right now, hoping to preserve his claims of primacy and have a shot at some of that prize money, despite being only partway to a full solution for N-S.
I don't think we see any behavior at all that isn't simple to understand and well described by the setup here, but tell me what you see differently.
OpenAI most certainly did not as you put it, "to act so aggressively". They have simply indulged in plagiarism/malpractice/fraud all for the sake of pumping up their evaluation in light of their forthcoming IPO and to one-up their arch-rival Anthropic and try to get themselves to AGI certification.
In the process they have shafted real-world hardworking mathematicians, which is to say the least, despicable. Note that stories are now coming out from other mathematicians who have also been shafted in a similar manner. Also there are cases where they have had mathematicians accept their "deal" (like the one they offered Buckmaster that he refused) and have OpenAI name linked to their work.
Regarding "their proof", their claim is only solving Navier-Stokes partially for when a smooth force is applied and not a fully general solution (which is maybe impossible). The proof is still being verified and we don't know whether it is just an approximation/hallucination or not.
Their most blatant lie is that they "gave only the problem statement" to their system which then went ahead and solved it. This is almost an impossibility. Problems like these need to identify a specific lead/approach and some work to be done on that path before you can even know whether that approach is promising and worth pursuing. This problem has resisted all attempts at solution for over two centuries. This is where the Buckmaster/Levent's work's importance comes in. They identified a promising approach based on other mathematicians work and have been using both OpenAI and Anthropic's models to make progress and had reached a promising milestone which they published. But they inadvertently gave away their approach to the model's training data set which OpenAI capitalized on by throwing a large amount of compute at the problem to get to the finish first.
This is straightforward stealing of other people's work and building upon it to claim it as your own which can and should be sued. All Scientists/Mathematicians/Researchers who feel OpenAI has done them dirty should band together and file suit.
This whole thing could easily have been avoided if they had worked with the researchers so everybody's concerns/needs are met.
By engaging in this sort of backstabbing, OpenAI has effectively killed the "Goose that laid the Golden Eggs". viz. Researchers were giving away their hard-earned highly specialized knowledge freely to the models in the hope that it will help them get quicker to the result. But now everybody is going to lockdown their research findings and will stop sharing it with the models to the overall detriment of advancement of Science.
As of 2024, ATS/Xanadu (ATS3) is being developed actively in ATS2, with the hope of reducing the learning needed by two main improvements:
- Adding an extra layer to ATS2 to support ML-like algebraic type-checking
- Type-based metaprogramming using algebraic types only
With these improvements, Xi hopes for ATS to become much more accessible and easier to learn. The main goal of ATS3 is to transform ATS from a language mainly used for research, into one strong enough for large-scale industrial software development.
Humans need to verify everything.
reply