Like discussed in other comments
Yes, I saw that afterwards. Sorry about that, and thanks for your answer.
you can prove consistency in a stronger theory
I get that. But:
- Even if you prove the consistency of Lean 4 in ZFC plus inaccessible cardinals, you then have to trust that theory, which, as far as I understand, has been less tested and challenged than plain ZFC?
- What surprised me was your apparently high confidence that such a proof exists and will be found. My impression was that such proofs are generally hard to find (I have in mind the indepen... (read more)
When people write Lean, they write using higher-level commands that the Lean kernel does not recognize. The process of turning high-level Lean code into something the kernel understands involves going through the Lean compiler, Lean elaborate, and Lean build system (Lake). All of these steps can fail, and result in a Lean program which accepts a proof of a false program.
EDIT: I asked Claude to fix the phrasing of my comment, and it informed me that, precisely, statements are elaborated too. So I guess that answers my question. I still leave it there in cas... (read more)
mathematicians have a pretty solid intuition for what statements are/aren't provable
Do you mean provable or decidable? And what makes you say that?
(The reason for my question is that:
- it sounds very weird that we could be quite certain that a statement is provable when no one at this time has been able to provide an actual proof (although it may only seem weird to me because I am not a real mathematician);
- my very small experience of research in mathematics (a PhD in proof theory) notably involved a conjecture that I was quite certain was true, until the guy across my desk proved it was false. ^^)
Assuming that Lean4 is consistent, then a proof should exist and we should be able to find it.
I am confused.
Given something like Gödel’s incompleteness theorems, I would have expected: “Even assuming that Lean4 is consistent, a proof may not exist”, and, given standard undecidability theorems: “and even if it did, we may not be able to find it.”
What am I missing?
I love the "we should stop seeking individual gain and start building something together that humanity can be proud of" vibe (if I'm not misreading you).
I also wonder:
- Whether the search for credit can be abandoned easily, or whether it has been deeply ingrained in us by millions of years of natural selection.
- For the same reason, whether people will stay motivated to work hard on difficult projects in a no-credit world.
How can we be sure that Mr. L didn't successfully design a clever system of compensators, and correctly validate that design using a sound spreadsheet?
Before reading further, here is my tentative answer.
The law of conservation of momentum that this machine would violate can be proved from Newton's laws of motion.
If Mr L. calculations are based entirely on Newton's laws, then what he has found is a contradiction in mathematics.
If they are based on different, incompatible laws of motion, then why should we trust those new laws?
I feel like that notion of different clustering algorithms should be included in the Human Guide to Words sequence. Love it!
I expect you already know some of these, but for anyone interested:
-
Asaf Karagila’s Anti-anti Banach–Tarski arguments. A short blog post whose main point is that “The axiom of choice is not at fault here. The axiom of infinity is.” As an illustration, he shows that if, instead of the axiom of choice, one assumes dependent choice and that all sets of reals are Lebesgue measurable, then there is a partition of the real line into strictly more parts than elements.
-
By the same author: Zornian Functional Analysis, or: How I... (read more)
Thank you for this detailed answer.
Some more questions:
notice if it's something that calls to you
I am not sure exactly what you mean here. From what I am reading, it is very difficult to know what it is without having experienced it. So how am I supposed to know? Do you have examples of motivations that would not be right?
(I would say that I personally feel very curious as to what it looks like, and that I would be significantly sad to learn that I can’t even try to get there.)
I highly recommend practicing as part of an organized community. […] You'r... (read more)
Ok. Thanks. So:
- p(bus has number ≤ 1546 | city has 2992 buses) = 0.5
implies
- p(city has < 2992 buses | bus has number 1546) = 0.5
?
If that is your reasoning, I do not see how you go from the former to the latter.
Is it a general fact that:
- p(bus has number ≤ n | city has N buses) = p(city has < N buses | bus has number n)
or does it work only for 0.5?
In that case, probability is n/N, and if we look for 0.5 probability, we get 0.5 = 1546/N which gives us N = 2992 with 0.5 probability.
Again, I am confused.
From what you write I understand this :
- p(bus has number ≤ n | city has N buses) = n/N
- so p(bus has number ≤ 1546 | city has N buses) = 0.5 iff. N = 2992
- therefore p(city has 2992 buses | bus has number 1546) = 0.5
But from your other comment, it looks like that last step and conclusion is not what you mean. Can you confirm that?
Or do you mean :
- therefore p(city has ≤ 2992 buses | bus has number 1546) = 0.5 ?
Or something else entirely?
That reminds me of How Go Players Disempower Themselves to AI. Even before an AI takeover, or absent one, this looks like a real danger for the generations currently being educated.