practal

13 ms·

121.
by practal 2y ago
A distribution is a function, on the space of test functions.
122.
by practal 2y ago
No, it is not the same, CH is just a particular instance of it, much like "shape" is not the same thing as "triangle".
123.
by practal 2y ago
I took a look at the book a while ago, and I like how it treats abstraction as its guiding theme. For my project Practal ( https://practal.com ), I've recently pivoted to a new tagline which now includes "Designing wi
124.
Show HN: Deep Dive into Abstraction Logic [video](youtube.com)
1 points by practal 2y ago|0 comments
125.
by practal 2y ago
I like both the ideas of 100r and of this rebuttal. I think much of this comes down to a fundamental misunderstanding, namely that code is the level at which we understand something . Rather, when we build software, we build a theory [1]
126.
by practal 2y ago
You might be misunderstanding here what the "goal" is. Your training metric is just another approximation of the goal, and it is almost never perfect. If it is perfect, you cannot overfit, by definition.
127.
by practal 2y ago
I've been thinking for quite some time about how to incorporate spacing properly into the syntax of a programming language, and I now settled for a simple solution: hard-code blocks of texts via spacing into the text format itself. I c
128.
by practal 2y ago
This is a great post, and full of inspiring ideas for what kind of work flows and features a modern theorem proving system could support.
129.
by practal 2y ago
This approach works very well, as far as I can tell so far: https://practal.com/press/aflap/1/ (mainly starting at "Syntactic Categories") I got it right only after finishing the draft of the articl
130.
by practal 2y ago
Van Plato's book seems interesting! I see that it has a chapter on natural deduction and sequent calculus. I found the focus on introduction and elimination rules in natural deduction always somewhat mystifying, and wondered about what
131.
by practal 2y ago
If you can represent algebraic geometry through mathematical objects, operations and operators, then yes. But I don't know algebraic geometry, so I cannot say if there would be any advantage of doing it in Abstraction Logic compared to
132.
by practal 2y ago
That's a very good point. I have been strongly influenced by Isabelle and Isar, which get a lot of things right. I think the future looks like this: The resulting text will be natural language (LLM powered), layering upon the actual fo
133.
by practal 2y ago
Type theory vs. set theory is not the only choice. It is possible to combine their strengths in a new foundation: A single mathematical universe, just as in set theory, and higher-order features and abstraction, just as in type theory. Note
134.
by practal 2y ago
I am writing about this here: http://abstractionlogic.com Chapter 1 of the book is already available (you can buy it for £0), and Figure 2 vs. Figure 3 describes how type theory is different from Abstraction Logic, although I do
135.
by practal 2y ago
Well, the most important difference is that Lean exists and is going strong, and Practal doesn't even exist yet. But the logic Practal is based on exists now. I am currently writing the basics of this logic up as a book [1]. Chapter 2
136.
by practal 2y ago
> So I don't really understand the point made in this post. I think you understand the point perfectly well. You just don't believe that there can be a logical system better suited to a foundation of mathematics than first-orde
137.
by practal 2y ago
Very smart to open up the project from the start to make collaboration possible. I have ambivalent feelings about this project. On one hand, I think this is great, it approaches things in the right way, and I think the project has a big cha
138.
by practal 2y ago
It is a very simple blog post, it makes a simple point, but I also think it is a very important point: Types are a means to an end. I am implementing Practal in TypeScript, and it is so much more productive than if I had to do it in JavaScr
139.
by practal 2y ago
Yes, this idea of collaborative proofs has been around for a while now, at least for 10 years: https://arxiv.org/abs/1404.6186
140.
by practal 2y ago
Exactly. Previous applications have taught me a lot about what VCs expectations are, and I know when I am fundable in their eyes. My ideas work and are a game changer. But until I can explain this clearly and have objective proof of that, I
141.
by practal 2y ago
I think applying to YC should be seen as fund raising activity. And pg's essays clearly state that fund raising is a distraction, so when you do that, just focus on it, and get it over with, so you can continue building. I must have ap
142.
by practal 3y ago
There are a LOT of natural numbers, even for an AI.
143.
by practal 3y ago
Yes, but you also need to make sure the input is correct! For example, your idea of automatically formalising a paper needs to somehow make sure that the result means the same as the paper.
144.
by practal 3y ago
It's great that top mathematicians are now interested in machine assisted proof. Love that my name appears in the talk (in small print) :-D Now I just have to somehow find funding for my project, Practal [1]. [1] https://pra
145.
Show HN: Recursive teXt(recursivetext.com)
2 points by practal 3y ago|0 comments
146.
by practal 3y ago
Ok, thank you, appreciate the "here be dragons"!
147.
by practal 3y ago
I've read up on CRDTs over the last two months or so (and I've come across your very helpful posts as well, of course), because I am building a collaborative editor for Practal [0]. In particular, I've invented a new simple t
148.
by practal 3y ago
Yes, there are different philosophies out there. > Fictionalism, on the other hand, is the view that (a) our mathematical sentences and theories do purport to be about abstract mathematical objects, as platonism suggests, but (b) there a
149.
by practal 3y ago
> Thinking purely conceptual notions are real is mysticism. No, it is not. We just have to disagree here. What is 1? What is 2? Is it real? Of course it is. Is 3.5 + πi real? Yes, because what are you talking about if it is not? Somethin
150.
by practal 3y ago
> It's just adding more mysticism to mathematics. No, it is actually the opposite. It is removing mysticism (which I hate) and adds clarity. There are real things out there, and we can go and use them for our purposes. These things

More ›