That's a very outdated text that is mostly irrelevant for modern maths except for its historical importance.
4,317 karma · joined October 31, 2019
I don't know if there's a way to remove axioms, nor do I think you can change the logical foundations (which are based in type theory).
I would say, "from a handful of axioms".
It's certainly true that when Euclid started this whole enterprise, it was thought thax axioms should be self-evident. But then, many centuries later, people discovered that there are other interesting geometries that don't satisfy the same axioms.
And when you get to reasoning about infinities, it's very unclear that anything about them can be considered self-evident (a few mathematicians even refuse to work with infinities, although it's definitely a very niche subcommunity).
Some of today's common axioms are indeed self-evident (such as "you should be able to substitute equal subterms"), but things like the axiom of choice have (at least historically) been much more controversial. I would probably say that such axioms can be considered "plausible" and that they generally allow us to be able to prove what we want to prove. But you'll definitely find mathematicians championing different axioms.
> Aside: I recall some famous mathematician had made a list of base proofs that you just hold to be true. Can someone remind me who, and/or what that list is called? I’m guessing they’re considered axioms.
That would be the ZFC axioms. It was originally the ZF axioms (named so after the mathematicians Zermelo and Fraenkel who worked in the early 20th century), and then later the Axiom of Choice (C) was added. It's generally considered to be the "standard" set of axioms for maths, although very few mathematicians actually work directly from these axioms. But in theory, you can take almost every mathematical proof (unless it's explicitly set in some other foundation) and recast it entirely in applications of the ZFC axioms.
(Although I wouldn't be surprised if somebody had already recreated something like Prolog in Lean with a tactic that does more or less what the Prolog interpreter does)
Are you talking about natural languages here? The so called Sapir Whorf thesis - in its strong or weak form - is rather controversial. There are some interesting findings, but the interpretation of them is still hotly debated.
In any case, none of the studies that I've seen (e.g. about colour perception, spatial reasoning, etc.) seem to be about syntax. I'd have to see some evidence that head-marking language speaker somehow think differently than dependent-marking language speakers and I haven't seen that.
> your argument ad absurdum is generally reasonable
it's a valid argument when somebody is speaking in absolutes, but I haven't seen GGP do that. There's a difference between saying "all syntax is completely arbitrary" and "syntax is not the point" - the latter suggests to me that if you stay within certain reasonable bounds (e.g. not be whitespace or malbolge), whether you use significant whitespace of braces, the language looks more like Pascal or like C, etc. are of minor importance in the grand scheme of things. Which is something you may disagree with, but it's a much more reasonable point that anything you can just counter with "but whitspace!".
Btw I'm not affiliated with Pony in any way, so I have no influence on what and how things could be improved in the docs.
With no intention of downplaying the particular scandal that you're referencing, I don't think this is correct. Victims of sexual abuse by the Catholic Church are also usually estimated to range in the thousands, particularly e.g. in Germany
https://en.m.wikipedia.org/wiki/Catholic_Church_sexual_abuse...
That appears to be your position (and maybe even that of a majority of developers), but it apparently isn't the position of the Pony developers. If you have a language in which you can mathematically reason about code (which Pony claims very prominently), then surface concerns such as syntax seem to matter less.
It's a different design goal and it feels like many people in the comments here don't appreciate that.
Apparently not too busy to visit HN and post shallow dismissals.
I agree with GP. Not everything is for everyone and expecting every project to cater to your very specific needs is rather entitled. If you're not interested, feel free to move on - I do that all the time for most of the content on here.
In Haskell:
1. Create a module with some datatype
2. Don't export the datatype's constructors
3. Export factory functions that guarantee invariants
How is that more complicated than creating a class and adding a custom constructor? Especially if you have multiple datatypes in the same module (which in e.g. Java would force you to add multiple files, and if there's any shared logic, well, that will have to go into another extra file - thankfully some more modern OOP languages are more pragmatic here).
(Most) OOP languages treat a module (an importable, namespaced subunit of a program) and a type as the same thing, but why is this necessary? Languages like Haskell break this correspondence.
Now, what I'm missing from Haskell-type languages is parameterised modules. In OOP, we can instantiate classes with dependencies (via dependency injection) and then call methods on that instance without passing all the dependencies around, which is very practical. In Haskell, you can simulate that with currying, I guess, but it's just not as nice.
However, it's not like you have to go out of your way to look for the complex numbers in some creative way. At some point while solving the quadratic equation you'll have to take the root of a negative number. So the only choice is to reach for the complex numbers, your hand is kinda forced.
no
This is distinct both from other typical IMO problems that I've seen and from research mathematics which usually do require some amount of creativity.
> exp(i\pi)+1=0
If your definition of "exp(i*theta)" is literally "rotation of the number 1 by theta degrees counterclockwise", then indeed what you quoted is a triviality and contains no nugget of insight (how could it?).
It becomes nontrivial when your definition of "exp" is any of the following:
- The everywhere absolutely convergent power series sum_{i=0}^\infty z^n/n!
- The unique function solving the IVP y'=y, y(0)=1
- The unique holomorphic extension of the real-valued exponential function to the complex numbers
Going from any of these definitions to "exp(i*\pi)+1=0" from scratch requires quite a bit of clever mathematics (such as proving convergence of the various series, comparing terms, deriving the values of sin and cos at pi from their power series representation, etc.). That's definitely not something that a motivated high schooler would be able to derive from scratch.
Agreed. A good abstraction usually doesn't obviate the need for understanding what's going on behind the scenes, it just means that I don't have to think about it all the time.
As a more extreme example, I don't usually think about the fact that the Java (or Kotlin, Scala, ...) compiler generates bytecode that runs in an interpreter that translates the bytecode to machine code on the fly. But sometimes it's useful to remember (e.g. when dealing with instrumentation).
Another example are things like databases, or concurrency constructs, etc. There it's usually good to know the properties they guarantee and one way to be able to reason through these is by having some understanding of how they're implemented under the hood.
what a bunch of nonsense
It can already be "cheaply verified" in the sense that if you write a proof in, say, Lean, the compiler will tell if you if it's valid. The hard part is coming up with the proof.
It may be possible that some sort of AI at some stage becomes as good, or even better than, research mathematicians in coming up with novel proofs. But so far it doesn't look like it - LLMs seem to be able to help a little bit with finding theorems (e.g. stuff like https://leansearch.net/), but to my understanding they are rather poor beyond that.
Let's not exaggerate. While I am often enough exasperated at how often certain restaurants or bars will still only accept cash (or sometimes EC card), I'm still able to do about 90% of my transactions by card.
It would be nice to add a disclaimer that this is a system you're working on.
> Exactly. They are seen as less valuable in the marketplace
I'm really confused as to how you think what you wrote follows from I wrote.
They're not seen as "less valuable", they're seen as more exploitable for chauvinistic reasons.
At no point did I say that the gender gap doesn't exist, how do you even come to that conclusion? My point is that "women should just demand less money" is a really bad takeaway from the gender pay gap. Maybe women should demand more money and/or unionise, and maybe men should help expose biases whenever they see them and demand transparent reviews. Just as an example, that's something works councils usually do where I live.
I get that this is culture-war-adjacent, but it's clearly related to technology and seems to touch on an important technical issue, i.e. biases in LLMs.
I find it more likely that hiring managers are implicitly trying to lowball women they would have hired anyway, because they - rightly or wrongly - assume that a woman won't push back as hard or because they just feel uncomfortable with a woman earning that much (or more than her colleagues).
One way to change that is to a) surface these biases, and b) encourage women to be as assertive in salary negotiations as men.