Smaug123

16 ms·

241.
by Smaug123 2y ago
Sure, I agree with everything you've said; I was sloppy in saying "Euclid's proof" (whose baroque language I haven't actually bothered to wade through) when I meant "the proof in the OP", though I was pr
242.
by Smaug123 2y ago
In that case your "It's much dumber than that, since he's invoking the law of the excluded middle to use contradiction at all." is simply false: you can use contradiction to refute a proposition without proving that
243.
by Smaug123 2y ago
Your statement is, I think, being wilfully sloppy. To quote the outline of the proof: "First Euclid assumed √2 was a rational number.". To quote the proof itself: "Euclid's proof starts with the assumption that √2 is equ
244.
by Smaug123 2y ago
(Important thing to do while understanding any theorem! Test the boundaries, discover what happens when you relax every hypothesis.)
245.
by Smaug123 2y ago
Then why didn't they! Of course the proof can be fixed, we all know sqrt(2) is irrational, but why get so close to proving it and then just not finish the job?
246.
by Smaug123 2y ago
No, "is not irrational" isn't the same as "is rational" without excluded middle; that's the whole point. (Equality of real numbers is not computable, so there is nonconstructive content to the implication &quot
247.
by Smaug123 2y ago
Could you please explain this? Clearly we both understand something completely different by either the term "excluded middle" or "contradiction". Note that Euclid's proof is intuitionistically valid, so it can&#x2
248.
by Smaug123 2y ago
As I said, according to the three sources above, which are the first sources I clicked on which didn't seem like blogspam, the phrase "proof by contradiction" is a term of art which means "uses the law of excluded middle
249.
by Smaug123 2y ago
Yep, that does work, although it needs a bunch of extra machinery (the fundamental theorem of arithmetic, which guarantees existence and uniqueness of prime factorisation). If you're happy to take that machinery as having already been
250.
by Smaug123 2y ago
https://en.wikipedia.org/wiki/Proof_by_contradiction , https://ncatlab.org/nlab/show/proof+by+contradiction , https://web.stanford.edu/class/cs103/guide_to_proofs#proo
251.
by Smaug123 2y ago
Euclid X prop 9. http://aleph0.clarku.edu/~djoyce/java/elements/bookX/propX9....
252.
by Smaug123 2y ago
FTA is massive overkill. For every number n, either n can be expressed as 2k for some k, or 2k+1 for some k, but not both (proof: by induction); in particular the square root can too. If the square root is (2k+1), then the square is 4k^2 +
253.
by Smaug123 2y ago
1) it's not a proof by contradiction, it's a proof of a negation :grump: 2) I am not a fan of this phrasing "we can't simplify forever". Why can't we? It's obvious if you phrase it in the usual way as &quo
254.
by Smaug123 2y ago
A language in which matching on a structure is not a statement but instead returns a value; the special case of matching on a boolean (this is often spelled `if`); one which doesn't have a `throw` statement (but instead models it as a
255.
by Smaug123 2y ago
You appear to have misread "expression" as "exception"; this is completely unrelated. An expression-based language is one that lets you do `let blah = if foo then bar else baz`, for example.
256.
by Smaug123 2y ago
Source for this submission: https://x.com/kupiakos/status/1820897820255338899 which links to a different crate; I selected this crate because it has orders of magnitude more downloads. > With the right tooling,
257.
No-panic: Attribute macro to require rustc to prove a function can't ever panic(crates.io)
2 points by Smaug123 2y ago|1 comments
258.
by Smaug123 2y ago
So it's famously difficult to write a correct date-time handling program, but my empirical observation is that it's considerably easier with a library like Noda Time which actually attempts to model some of the domain beyond &qu
259.
by Smaug123 2y ago
This is really not the kind of problem LLMs are bad at! But since you insist, given the LaTeX, Claude 3.5 Sonnet correctly stated the theorem in full while inventing notation for the floor operation (it did correctly note unprompted what th
260.
by Smaug123 2y ago
Could you clarify that? Are you saying you wish everything could be inline by default? (It's not true that things are currently inline by default.)
261.
The Infinity Machine(chiark.greenend.org.uk)
69 points by Smaug123 2y ago|40 comments
262.
by Smaug123 2y ago
… no? After the LaTeX output, I told stock GPT4o that the answer was "all even integers", and asked for the statement in Lean. I had to make two changes to its output (both of which were compile-time errors, not misformalisation
263.
by Smaug123 2y ago
(You're talking to one of the people who was part of the project, which is why I took @ocfnash's answer as authoritative: they did not cheat.)
264.
by Smaug123 2y ago
FWIW, GPT-4o transcribed a screenshot of problem 1 perfectly into LaTeX, so I don't think "munge the problem into machine-readable form" is per se a difficult part of it these days even if they did somehow take shortcuts (whi
265.
by Smaug123 2y ago
I'm attacking nobody! I literally couldn't understand the point, so I said so: as stated, its premises are simply clearly false! Your point, however, is certainly a good one: IMO problems are an extremely narrow subset of the sp
266.
by Smaug123 2y ago
I think you might be thinking of the recent project to start Fermat's Last Theorem? The Riemann hypothesis has been easy to state (given what's in Mathlib) for years.
267.
by Smaug123 2y ago
Nope, per Oliver Nash who worked on the thing: https://news.ycombinator.com/item?id=41070372
268.
by Smaug123 2y ago
So I am extremely hyped about this, but it's not clear to me how much heavy lifting this sentence is doing: > First, the problems were manually translated into formal mathematical language for our systems to understand. The non-geom
269.
by Smaug123 2y ago
And while AlphaProof is clearly extremely impressive, it does give the computer an advantage that a human doesn't have in the IMO: nobody's going to be constructing Gröbner bases in their head, but `polyrith` is just eight chara
270.
by Smaug123 2y ago
I really don't understand what you mean by this. 1) it's not known whether chess is a win for White or not. 2) IMO problems, such as 2024 problem 1 which the system solved, are often phrased as "Determine all X such that…&quo

More ›