practal

6 ms·

1.
The End of Mathematics(daniellitt.com)
33 points by practal 1mo ago|20 comments
2.
by practal 1mo ago
Isabelle is actually a "logical framework", so it supports intuitionistic logic, actually its meta theory is intuitionistic higher-order logic. So this is not because of the logic, it is because of the mindset. Intuitionistic lo
3.
by practal 1mo ago
> So you get complex recursion and inductive definitions baked into the kernel. It is a pragmatic choice, just like a type system is. I think both of these choices are outdated now that formalisation is fast. What you really want is a si
4.
by practal 1mo ago
I added proof objects ages ago to HOL Light, it is not a big deal. It's just, as Larry said, why would you want them in the first place?
5.
by practal 2mo ago
So what happens with optimistic local operations that become invalid after replay of canonical operations? Are they just thrown away as well?
6.
by practal 2mo ago
One of my favourite books of all time is by her: The Dispossessed. It "features the development of the mathematical theory underlying a fictional ansible, a device capable of faster-than-light communication, which can send messages wit
7.
by practal 2mo ago
I actually think it is just the dawn of mathematics. During the last few days I discussed a few questions about abstraction logic [1] with AI that I was wondering about for quite some time (years), but didn't have the time + energy + i
8.
by practal 3mo ago
I think 6) is a very good point. The simple reaction to it is, well, I just define a small verification kernel that I trust, and the rest is just scaffolding that does not need to be trusted in order to have full confidence in the verificat
9.
by practal 3mo ago
TU Munich and Nipkow, Makarius et.al. are also at the center of the influential Isabelle theorem prover. TU Munich is cool :-)
10.
by practal 3mo ago
I agree with that, that's why I am starting with plain syntax first in https://zero.practal.com , because that is really where all the information/logic lives. But there will also be a presentation layer on top of that,
11.
by practal 3mo ago
How did you get suspended for 8 hours, given a 5-hour window? Maybe you are prompting it wrong [1]. [1] https://www.wired.com/2010/06/iphone-4-holding-it-wrong/
12.
by practal 3mo ago
I used it yesterday afternoon-night and this morning-afternoon, UK time, over a period of a few 5-hour windows. I didn't count the prompts, wall time was 1d6h, API time was 2h10m.
13.
by practal 3mo ago
I am quite impressed with Fable 5. I used the £18 subscription, and asked it to convert the document processing of Practal Zero [1] from running in the same thread as the UI to a worker thread. Just two days before I gave the same task to C
14.
by practal 4mo ago
To add, what also often happens in these discussions is that Codex suggests a design that makes no real sense at all, or that it brings up two or three design alternatives, and recommends exactly the wrong one.
15.
by practal 4mo ago
On Saturday I thought I had vibe coded myself into a mess. I had implemented a new block type in my structured editor for Practal Zero (or rather let Codex do it), and suddenly the syntax highlighting broke in the whole document. Asking Cod
16.
by practal 4mo ago
Super. I always wanted to learn about sheaves and schemes and the like, and this gives a simple introduction that really motivates digging deeper into the details. It is also immediately clear why this plays a role in semantics for logics:
17.
by practal 4mo ago
> Even more important than lemmas are observations, but that is another story. In my book about abstraction logic ( http://abstractionlogic.com ) I have definitions, theorems, lemmas, and even observations :-) Just did a count
18.
We're excited to announce that AXLE is switching from Lean to Rocq(axle.axiommath.ai)
3 points by practal 6mo ago|1 comments
19.
by practal 6mo ago
> After mass feedback from the public, we're excited to announce that AXLE is switching from Lean to Rocq. The new name will be AXRE (Axiom Rocq Engine). All existing Lean proofs will be automatically translated using GPT-2. Just s
20.
by practal 6mo ago
Print-on-demand Amazon paperback books can have great quality. It is mainly the responsibility of the author, by doing proper layout, and choosing a nice paper option. I've self-published with Amazon KDP, and am really happy with the r
21.
by practal 6mo ago
Just two days ago I was curious about the PhD advisor of my PhD advisor and so on, and discovered that I am actually an academic great-grandson of Hoare (shame on me, I should have realised that earlier), and joked, "Wow, they are all
22.
by practal 8mo ago
I think that is a very good point. Code is definitely not worthless, but I don't think that capitalism has the right tools for pricing it properly. I think it will become a lot like mathematics in that way.
23.
by practal 8mo ago
I see the current generation of AI very much as a thing in between. Opus 4.5 can think and code quite well, but it cannot do these "jumps of insight" yet. It also struggles with straightforward, but technically intricate things, w
24.
by practal 9mo ago
In principle, this is how these systems work. In practice, there are usually plenty of things that make it difficult to say for sure if you have a proof of something.
25.
by practal 9mo ago
You know what? I agree with you. I have not formalised any of my stuff on abstraction logic [1] for that reason (although that would not be too difficult in Isabelle or Lean), I want to write it down in Practal [2], this becoming possible I
26.
by practal 9mo ago
Ideas and correctness depend on each other. You usually start with an idea, and check if it is correct. If not, you adjust the idea until it becomes correct. Once you have a correct idea, you can go looking for more ideas based on this. For
27.
by practal 9mo ago
> Well, assuming it's free of escape hatches like `sorry` There are bugs in theorem provers, which means there might be "sorries", maybe even malicious ones (depending on what is at stake), that are not that easy to detect
28.
by practal 10mo 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
29.
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
30.
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

More ›