61–70 of 96 posts
I still can't believe that we are in the era of 'star trek' like "Computer plot me a proof for this math problem" in my life time! Wish we could also do the same for "Beam me up scotty"
> Wish we could also do the same for "Beam me up scotty" You might die every time you do, though, so maybe not.
Earlier quoted context omitted.
I'm not a mathematician, but how credible is that anti-Lean material? Are they marketing an alternative programmatic approach, as in they're anti-lean because "I got something else" or are they philosophically anti-Lean and have valid arguments?
It seems pretty obviously machine generated, and the appearance of the word "metaphysics" in the output suggests the prompt author didn't know what they were talking about to begin with.
Or the author is not natively fluent in English.
Having the ability to throw math heavy ML papers at the assistants and get simplified explanations / pseudocode back is absolutely amazing, as someone who's forgot most of what I learned in uni, 25+ years back and never really used it since.
How do you verify that the explanation is accurate? Mathematical definitions can be very subtle.
“The argument used some p-adic algebraic number theory which was overkill for this problem. I then spent about half an hour converting the proof by hand into a more elementary proof, which I presented on the site.”
What’s the exchange rate for 30 minutes of Tao’s brain time in regular researcher’s time? 90 days? A year?
Earlier quoted context omitted.
> Wish we could also do the same for "Beam me up scotty" You might die every time you do, though, so maybe not.
that also brings the philosophycal question of will I be the same if all my atoms and molecules are copied exactly the same?
Earlier quoted context omitted.
I could be wrong, but FWIW I doubt Hungarians include diacritics that don’t exist in Hungarian (like ñ) when writing foreign names.
Depends. There are names that are "romanized" to Hungarian pronunciation rules, like Dosztojevszkij (Dostoevsky), or Kolumbusz Kristóf (Cristoforo Colombo - Hungarian puts the family name first), though it is no longer the practice, it's mostly used for historic names only. That is, Trump is written like that, and not as we would pronounce (something like "Trámp") In general, if the source language has a latin alphab…
Earlier quoted context omitted.
that also brings the philosophycal question of will I be the same if all my atoms and molecules are copied exactly the same?
Thinking about such questions before we are capable of doing such an experiment at least with small animals is like discussing how many angels can stand on the point of a pin.
Earlier quoted context omitted.
Depends. There are names that are "romanized" to Hungarian pronunciation rules, like Dosztojevszkij (Dostoevsky), or Kolumbusz Kristóf (Cristoforo Colombo - Hungarian puts the family name first), though it is no longer the practice, it's mostly used for historic names only. That is, Trump is written like that, and not as we would pronounce (something like "Trámp") In general, if the source language has a latin alphab…
How would you write e.g. the Spanish surname Yáñez ?
Earlier quoted context omitted.
Isn't there a risk that you're engaging with an inaccurate summarization? At some point inaccurate information is worse than no information. Perhaps in low stakes situations it could at least guarantee some entertainment value. Though I worry that folks will get into high stakes situations without the tools to distinguish facts from smoothly worded slop.
There is, but there is an equal risk if you were to engage about any topic with any teacher you know. Everyone has a bias, and as long as you dont base your worldview and decisions fully on one output you will be fine.
Earlier quoted context omitted.
It's mainly the latter, although the author makes half-hearted gestures as some sort of CAS (Computer Algebra System) being better. It's not very credible. There are individual fragments that make sense but it's not consistent when taken together. For example, by making reference to Godelian problems and his overall mistrust of infinitary structures, he's implicitly endorsing ultrafinitism (not just finitism because…
I wonder what the ultrafinist argument against theorems about the natural numbers as defined in Coq would be.
The classical mathematician would respond that the theorems are clearly meaningful and you can easily test them against any natural numbers you care about to see empirically they are meaningful.
The ultrafinitist would respond that they are only coincidentally correct, in the same way that pre-modern mathematical reasoning was often very sloppy, featured regular abuse of notation, and had no coherent foundations, but nonetheless still often arrived at correct conclusions by "coincidence."
The classical mathematician might then go over how strong the intuition of something like "there exists a number that..." is and how it is an easily empirically validated statement...
And so the debate would keep going.
Having the ability to throw math heavy ML papers at the assistants and get simplified explanations / pseudocode back is absolutely amazing, as someone who's forgot most of what I learned in uni, 25+ years back and never really used it since.
This is where LLMs shine for learning imo: throwing a paper in Claude and getting an overview then being able to ask questions. Especially for fields that I didn’t study at the Bachelors or Masters level, like biology. Getting to engage with deeper research with a knowledgeable tutor assistant has enabled me to go deeper than I otherwise could.