Can you please help me understand where you are having difficulty reading the comment? I am genuinely interested. It seems I need to improve my writing skills.
To sum it up in one sentence: You don't need to explain words that I can look up in a dictionary, unless you are commenting on that explanation. I know what the word "joke" means but you are forcing me to either read the definition or look for where you continue your comment. It's also slightly demeaning since I can read this as "you don't know what the word joke is, let me explain it to you". You do this again for the words formula, garden and absurdity. If you really need to give extra details to a word that you are using, you can do it in brackets (like this) or with a footnote [1].
The definitions of the words formula and garden also seem out of place because they don't add anything to what you were saying -- at least I don't see any analogies that would make the joke funnier.
> Another way to look at what irrational numbers are is to say that they sort of don't really exist, they are like limits, or some ideals that cannot be reached because you'd need to spend infinity to reach that exact number when counting, measuring etc.
Depending on your definition of "existence", rational numbers (or any numbers) don't exist either.
I think it's kind of obvious what my definition of existence could be from the answer above: if it's possible to count up to that number in finite time, that number exists. By counting I mean a physical process that requires discrete non-zero intervals between counts. And you don't have to count in integers, you can count in fractions, not necessarily equal at each step: the only requirement is that the element used for counting exists (in terms of this definition) and that you are able to accomplish counting in finite time.
To me, this pretty much captures what people understand the numbers to be used for outside of college math (so no transfinite, cardinals etc.)
Do you mean the computable numbers? (there's an algorithm to compute them to arbitrary precision)
The irrational numbers used outside of college math, like pi or e or sqrt(2), are computable, though almost all are not.
You can do a lot of productive math using just computable numbers since they form a real closed field [1]. I believe they're a little harder to work with though.
Computable numbers are those that are described by computable functions. Irrationals like pi can be described by computable functions that take a precision as input.
Yeah... the article has a lot of "simplifications" that the reader has to just kind of trust the author on... and those are meant for people with not a lot of mathematical sophistication. All this talk about "shrink fast enough" and why it's important is just some intense handwaving w/o any actual explanation.
To be fair, it's kind of upsetting, but maybe there's no way to help it... some mathematical proofs can be "dumbed down" to the point that people with very little background can understand them. The proof of sqrt(2) being irrational might be one of those. But, what's given in the article feels like either the author didn't really understand the subject, or she couldn't explain what she understood in simple terms. But, it's really rare that there's such an easy to understand proof or concept. So, I don't blame her.
I don't think that computers have an advantage because they can navigate search spaces efficiently. The search space for difficult theorems is gigantic. Proving them often relies on a combination of experience with rigorous mathematics and very good intuition [1] as well as many, many steps. One example is the classification of all finite simple groups [2], which took about 200 years and a lot of small steps. I guess maybe brute forcing for 200 years with the technology available today might work. But I'm sceptical and sort of hope that I won't be out of a job in 10 years. I'm certainly curious about the current development.
Oh for sure, when I say "soon" it's only relative to AGI.
What I meant to convey, is that theorem proving at least is a well-defined problem, and computers have had some successes in similar-ish search problems before.
Also I don't think pure brute-force was ever used to solve any kind of interesting problem.
Chess engines make use of alpha-beta pruning plus some empirical heuristics people came up with over the years. Go engines use Monte-Carlo Tree Search with straight deep learning models node evaluation. Theorem proving, when it is solved, will certainly use some kind of neural network.
