Tainnor

35 ms·

661.
by Tainnor 2y ago
Mathematics education seems to be really different depending on the country (I'm in Europe). I barely saw a proof (except maybe some geometry proofs) in any of my high school maths classes and had to learn what a mathematical proof is
662.
by Tainnor 2y ago
> to allow irrationals I think you need some real analysis (it's been a while, but I think the usual way is to first define exp and log, and then say that a^b=exp(b*log(a)), which is kind of cheating because we have to define exp fi
663.
by Tainnor 2y ago
> which you can easily verify is its own derivative simply by differentiating it term-by-term. Yes, but it's not a priori clear that the series actually even converges for all x, and the fact that power series are differentiable ter
664.
by Tainnor 2y ago
Theoretical impossibility results like this one are often interesting because they tell you there is no "smart" way even in practice beyond just brute forcing it. While it's true that the class of programs that terminate in t
665.
by Tainnor 2y ago
If you fix a particular axiom system for deriving your termination proofs (e.g. because you write them all down in Coq), then for Gödelian reasons, there are programs that don't terminate but for which a nontermination proof doesn&#x27
666.
by Tainnor 2y ago
> there's even a prigramming language that only accepts programs that do so, Idris. If you declare every function total. Idris still allows partial functions, and you can even cheat the whole system with "assert_total". Of
667.
by Tainnor 2y ago
I suspect what GP means is that for certain programs, (assuming a fixed set of axioms) there exists neither a proof of its termination nor of its non-termination (not just that we can't find it; it doesn't exist). Of course, if th
668.
by Tainnor 2y ago
> Figuring out whether a single given program halts is decidable It's maybe nitpicky, but by definition "decidable" applies to a language, i.e. a set of programs, not a single program. Of course, there is a trivial TM (eit
669.
by Tainnor 2y ago
For example, here's a formally verified proof in Lean: https://github.com/leanprover-community/mathlib4/blob/124731...
670.
by Tainnor 2y ago
That's what we thought over in Germany. Then, against all odds, we got this weird centre-left-libertarian coalition government that can't agree on almost anything (especially not budgets), but one thing they could agree on was leg
671.
by Tainnor 2y ago
Please don't configure important things in the IDE. IDE configs are notoriously fickle and checking them into the repo usually just leads to a lot of problems in my experience, plus it will mean duplicated effort every time you need to
672.
by Tainnor 2y ago
Their definitions of OOP and FP are rather restrictive - it's basically FP = ADTs (data) and OOP = interfaces (codata). Many modern languages support both (e.g. Haskell has typeclasses, Java has records and sealed interfaces).
673.
by Tainnor 2y ago
> Especially with computer proof systems growing in popularity there's an increase in the interest in constructive methods. I think one big reason Lean is much more popular among mathematicians than Coq ever was is that Lean is pret
674.
by Tainnor 2y ago
> because type theory can be verified by a computer proofs in FOL can be checked by a computer without any need for type theory - just look at metamath.
675.
by Tainnor 2y ago
Well, you've been claiming that these advances are "super important" and that set theory is not rigorous, but you have provided no evidence for either claim.
676.
by Tainnor 2y ago
The point "most of actually useful mathematics can be recast into a constructive framework" is a much more reasonable one than your previous one, that Cantor's work was "hot garbage" (even though of course diagonali
677.
by Tainnor 2y ago
It's really hard to see the history of the sciences especially in the last couple of centuries as anything but a resounding success of modern mathematics. Whatever qualms some people may have about classical mathematics, nobody has sho
678.
by Tainnor 2y ago
What important discoveries have you made using your supposedly "more rigorous" mathematics?
679.
by Tainnor 2y ago
The current government coalition is threatened by the CDU (centre-right), not by Linke (that has almost no voters left) or AfD (who no other party wants to form a coalition with). The most likely outcome after the next election at this poin
680.
by Tainnor 2y ago
I don't understand the point of your comments.
681.
by Tainnor 2y ago
More generally, Cantor's diagonal argument shows that there is no surjective map of a set onto its powerset.
682.
by Tainnor 2y ago
fun n => 0 I'm not sure what you're trying to disagree with here.
683.
by Tainnor 2y ago
It's 100% possible to base logic and proof theory off of set theory. For example, you can treat proofs as natural numbers via Gödel encoding (or any other reasonable encoding) and we know that natural numbers can be represented by sets
684.
by Tainnor 2y ago
You can't map the natural numbers to the set of real numbers, but you can map the natural numbers to the fractional part of a single real number.
685.
by Tainnor 2y ago
I agree that "I ran out of things to watch/read" is something I find puzzling. There are so many great books, shows, movies, musical compositions, ... I don't know how anyone could ever run out.
686.
by Tainnor 2y ago
Yes.
687.
by Tainnor 2y ago
Books are media too. I've been an avid reader from early childhood and I don't consider my life boring. I guess what a "boring life" is, is up to every individual.
688.
by Tainnor 2y ago
The thing that both of your goals have in common is that they require software which is architected and not just an interconnected mess of everything calling everything else. If you do have such a mess, you can't really get a good visu
689.
by Tainnor 2y ago
Kotlin
690.
by Tainnor 2y ago
I was maintaining a server-side app written in Swift from 2018 to 2020 and we ran into tons of issues at least back then. I haven't looked into all the improvements they did since, but you might want to check. My coworker wrote down so

More ›