practal

7 ms·

31.
by practal 11mo ago
See, I don't get why people say that the world is somehow more complex than the world of mathematics. I think that is because people don't really understand what mathematics is. A computer game for example is pure mathematics, min
32.
by practal 11mo ago
There is a proof as part of my thesis that the engine is correct, but it is not formal in the sense of machine-checked. Note that the final result of the Flyspeck project does not depend on that proof, as the linear inequalities part has la
33.
by practal 11mo ago
As I said, it depends on how you practically implement it. I've used it for proving linear inequalities as part of the Flyspeck project (formal proof of the Kepler conjecture), and there I implemented my own rewrite engine for taking a
34.
by practal 11mo ago
Yes, indeed, a proof proves what it proves. You confuse spec and proof.
35.
by practal 11mo ago
The basic idea is: You run a program F on some input x, obtain r, and then you have some sort of justification why F x = r is a theorem. There are various levels of how you can do this, one is for example that "running the program&quot
36.
by practal 11mo ago
No, that misunderstands what a proof is. It is very easy to write a SPEC that does not specify anything useful. A proof does exactly what it is supposed to do.
37.
by practal 1y ago
In principle, LLMs can do this already. If you ask Claude to express this in simple words, you will get this translation of the theorem: "If applying f to things makes them red whenever they're not already red, then there mu
38.
by practal 1y ago
Indeed, and e:t in type theory is quite a strong ontological commitment, it implies that the mathematical universe is necessarily subdivided into static types. My abstraction logic [1] has no such commitments, it doesn't even presuppos
39.
AI for Math Winners(renaissancephilanthropy.org)
1 points by practal 1y ago|0 comments
40.
by practal 1y ago
You could, there is no fixed syntax for arrays in Practal, so it would depend on which custom syntax becomes popular. But for expressions that are bracketed anyway, it makes sense to have commas (or other separators), because otherwise you
41.
by practal 1y ago
Sure, color and indentation are optional, but even without those, I don't see that a comma in the above syntax helps much, even on a 80x24 monochrome display. If you want separators, note that the labels which end with a colon are just
42.
by practal 1y ago
Oh, actually that is the syntax I will use for writing abstractions: my-abstr x y z foo: "bar" baz: "bak" "quak" quux: [a, b, c, d] lol: 9.7E+42 I don't think my-abstr x y z, foo: "bar&
43.
by practal 1y ago
Wondering if someone on HN came across a solution to this before?
44.
Persistent sequences with insert and delete and canonical structure?(cs.stackexchange.com)
1 points by practal 1y ago|1 comments
45.
Three challenges in machine-based reasoning(amazon.science)
1 points by practal 1y ago|0 comments
46.
by practal 1y ago
Wow. I am glad your problems are not my problems.
47.
by practal 1y ago
All the information you need to know about that article is right at the top of it [1]. I am very clear that this is a conversation with a Claude impersonation of Graham Priest, not Graham Priest himself. I don't see what is unethical a
48.
by practal 1y ago
Good one! (Q)Basic was my first language. Well, my second really, after .bat files.
49.
by practal 1y ago
In Terence Tao's book "Compactness and Contradiction", at the very start on page 1, he introduces material implication "If A Then B" (or "A implies B") as "B is at least as true as A", and then l
50.
by practal 1y ago
Exactly. Clearly LLMs are not magic, so why do people insist that using LLMs is the same as believing in magic?
51.
by practal 1y ago
Going from informal to formal can be done using autoformalization [1]. The real question is, how do you judge that the result is correct? [1] Autoformalization with Large Language Models — https://papers.nips.cc/paper_files&
52.
by practal 1y ago
Yes, you just don't understand :-) I am working on making it simpler to understand, and particularly, simpler to use . PS: People keep browsing the older papers although they are really outdated. I've updated http://ab
53.
by practal 1y ago
My answer is already in my previous comment: if you have two formal languages to choose from, you want the one closer to natural language, because it will be easier to see if informal and formal statements match. Once you are in formal land
54.
by practal 1y ago
Does any popular MCP host support sampling by now?
55.
by practal 1y ago
If first-order logic is already sufficient, why are most mature systems using a type theory? Because type theory is more ergonomic and practical than first-order logic. I just don't think that type theory is ergonomic and practical en
56.
by practal 1y ago
> Being so similar to programming languages I think it is more important to be close to English than to programming languages, because that is the critical part: "As close to a programming language as necessary, as close to English
57.
by practal 1y ago
> The problem with trying to make "English -> formal language -> (anything else)" work is that informality is, by definition, not a formal specification and therefore subject to ambiguity. The inverse is not nearly as dif
58.
by practal 1y ago
You would definitely think so, Lean is in a great position here! I am betting though that type theory is not the right logic for this, and that Lean can be leapfrogged.
59.
by practal 1y ago
Great talk, thanks for putting it online so quickly. I liked the idea of making the generation / verification loop go brrr, and one way to do this is to make verification not just a human task, but a machine task, where possible. Yes,
60.
by practal 1y ago
If you have different representations of the same thing (llms.txt / HTML), how do you know it is actually equivalent to each other? I am wondering if there are scenarios where webpage publishers would be interested in gaming this.

More ›