It doesn't, at all. Unlike the US (and to a lesser extend, Europe), Chinese do not have a majority of their wealth invested in stocks.
Besides, the Chinese st9ck market has been atrocious since.... pretty much forever. You'd think they still live in mud pools if you think the stock market is representative of overall development.
Rich people in general have this belief, that they somehow got there by objective means and via their superior intellect. I just watched an interview the other day that someone posted where Sam Altman described using a notebook (yes literally pencil and paper) but was describing it as if he had discovered fire. These people are literally blinded by their money.
Lean is a theorem prover. If it "compiles", and the proposition as coded in Lean is equivalent to what the theorem proposes in natural language, the theorem is correct. https://en.wikipedia.org/wiki/Lean_(proof_assistant)
I don't understand then, because it doesn't sound like you understand how Lean works.
The actual proposition of the theorem is very short in Lean, and at this point has been looked at by probably hundreds of mathematicians (including the authors of the article). All that needs to be confirmed manually is that the proposition statement matches what people say the theorem actually proves. That has been done.
At that point, the rest of the actual proof steps are automatically verified by Lean - that's literally the entire point of Lean. There is no additional verification step - "What has shown the Lean proof to be correct" is the fact that the Lean program automatically validated it and generated a certificate.
But what mathematicians really care about is the actual steps. What the authors of the article have shown is just because you have a Lean program it doesn't mean the steps of the natural language theorem have been "autoformalized", because there is no guarantee the steps from the natural language description match the Lean code.
A Lean program that compiles proves what it states. The question is whether the program states what we think it does. If I recall, this program is 12 million lines long. Mathlib is not perfect, and it's not hard at all to have a Lean statement that isn't what you think it is.
So my question is whether people have actually checked that the generated program, all 12 million lines of it, has the statements that are expected.
But that's where you're wrong. All 12 million lines do not need to be checked (again, that's literally the entire purpose of Lean). All that needs to be checked is that the proposition of the theorem is what we think it is, and that has been done. What Lean guarantees is that if you start with a set of axioms -> whole bunch of steps that nobody really ever needs to read -> final theorem proposition, that those steps do successfully prove the theorem.
You say "it's not hard to have a Lean statement that isn't what you think it is", and that's true - indeed, what the entire paper is about is that the intermediate steps in Lean don't match the natural language description. But the statement of the proof in Lean (which again is quite short) is what we think it is, and hence the Lean proof is valid.
That's extremely hard to believe. First, one question arises: what are the 12 million lines doing if they're not needed? Secondly, don't those 12 million lines build up the theory that is eventually proved? Mistakes could be there that makes the outer statement seem like something it isn't, could there not be?
There's maybe an even simpler way of illustrating this.
Fermat's Last Theorem is very easy to state. There are no positive integers a, b, and c such that a^n + b^n = c^n. This likewise easy to write in Lean. The statement of the theorem is exactly one line of code.
theorem fermat_last_theorem (n : ℕ) (n_ge_3 : 3 ≤ n) (a b c : ℕ) (a_is_positive : 0 < a) (b_is_positive : 0 < b) (c_is_positive : 0 < c) : a ^ n + b ^ n ≠ c ^ n
Kevin Buzzard's team of human mathematicians attempted to prove this in Lean. They got to about 60000 lines of Lean code and were not anywhere close to finishing the job.
Anthropic came around with a Claude model that proved it in 13 million lines of code. (Buzzard's team might have ultimately used within the same order of magnitude if they finished. It's very unclear. They were at minimum years away.)
Whether 60000 or 13 million, only one line of code was necessary to manually verify whether they had successfully proved Fermat's Last Theorem, just the statement of `fermat_last_theorem`. None of the rest of the code built up the theory at all.
Indeed if those lines of code built up the theory, that would suggest that the statement of Fermat's Last Theorem is incomprehensible, if professional mathematicians cannot define Fermat's Last Theorem in even 60000 lines of code! But that's pretty absurd. You can explain the statement of Fermat's Last Theorem, completely rigorously, to a middle schooler.
> First, one question arises: what are the 12 million lines doing if they're not needed? Secondly, don't those 12 million lines build up the theory that is eventually proved? Mistakes could be there that makes the outer statement seem like something it isn't, could there not be?
This seems to reflect an incorrect understanding of formal mathematics.
Formal mathematics can be thought of as a game with rules where a statement to be proved is some game end state. If you play 12 million valid moves and arrive at the desired end state then you have proved that the statement is valid. If your logical system is sound (e.g. first order logic), then you have proved your statement is true.
The entire point of the formalization of logic and mathematics through the 19th and 20th centuries was to unlock this capability. Such that, if you only care about whether your statement is true or not and not why it's true, the intermediate steps are entirely unnecessary.
To answer each of your questions:
> First, one question arises: what are the 12 million lines doing if they're not needed?
They are the intermediate computations necessary to show that the final statement is valid. This is much like intermediate arithmetic operations in a large complicated arithmetic expression. As long as you believe that the computer can calculate each individual arithmetic expression correctly, you don't need to manually review the billions of intermediate calculations that result in the final number.
> Secondly, don't those 12 million lines build up the theory that is eventually proved?
No. Not in the way you're thinking of. It seems you are using "theory" to mean the concepts necessary to express the statement itself. This is a very different set of lines than the proof itself (and generally much much more compact). Very difficult to prove statements can be stated in very simple language. Often the theory is <0.01% of the total lines of code.
> Mistakes could be there that makes the outer statement seem like something it isn't, could there not be?
No. Only the language used in the final statement can cause this issue, i.e. the theory. The intermediate 12 million lines cannot affect this, assuming your computer can carry out arithmetic correctly.
Another way of thinking about it is that the big breakthrough of 19th and 20th century mathematical logic is to conclusively show that formal mathematics is fundamentally just a set of arithmetic operations.
Hence in a very real sense, proving a mathematical statement is exactly identical to finding x in an arithmetic expression f with some constant k such that f(x) = k, where k is determined by the statement you wish to prove (not the 12 million lines).
Showing that x causes f(x) to equal k is exactly equivalent to proving the mathematical statement associated with k.
The 12 million lines are an alternative notation, no different in spirit to decimal notation or binary notation, of writing down x. It is some gigantic natural number.
You must understand k. If you use the wrong k, then you have proved another statement than what you intended. This is usually about a dozen lines of code.
You must be confident in the correctness of f. This corresponds to the believing that your type checker (since Lean uses dependent typing as its method of proof checking) has no fundamental soundness bugs. This can be controversial and indeed Lean's type checker has had soundness bugs in the past! But crucially f does not depend on k or x. Every time you fix a bug in f you can rerun it for any k or x you care about.
But you don't have to actually read all the digits of x, in whatever notation you care about. You can copy paste it in from some gigantic file handed to you by a stranger. As long as f(x) = k, you know that you have proved the mathematical statement associated with k.
Overall, this is roughly like asking why you trust a computer to solve a long division problem that has 12 million intermediate steps if you don't actually read all 12 million intermediate steps yourself. Well I trust the computer to do one step of division correctly and to be able to repeat that faithfully 12 million times. Hence I trust the computer can solve a long division problem involving millions of digits, even if I don't actually look at all 12 million intermediate computations myself.
What do you mean by native target in this instance? Since you mentioned Rust, which is a systems language that compiles to native with no runtime, and Go, which has a garbage collector and runtime, as examples I'm a little confused.
> I'd say if you know and like Rust, then Gleam should be easy to pick up
I think by sentiments like this, people mean if you know unions, records, and pattern matching then you'll more easily pick up another language that has unions, records, and pattern matching.
Right, and I’m explaining that my multiple years of experience teaching and helping newcomers that an expectation of similarity to Rust frequently results in difficulty, and that it is beneficial to downplay any perceived link.
There are awkward things. For example, if you ingest a nanosecond resolution timestamp, there's no way to re-export that out of the Polars dataframe with nanosecond resolution.
I'm not sure this is true e.g. you can specify schema `pl.Datetime("ns")`. That survives roundtrip to/from parquet in my experience. True though that the default is `us` whereas pandas defaults to `ns`.
What does the stock market have to do with anything?
reply