practal

5 ms·

1.
by practal 7d ago
Seems to me to be two different sides of the same coin. Pedagogy is about finding a way to communicate to me an idea based on my intuition and seeing things. A research exposition is about presenting the idea in terms of your intuition and
2.
by practal 7d ago
One example is what currently plays out, see the previous guest post on Tao's page: https://terrytao.wordpress.com/2026/09/12/after-math/ The blog post says that the statement "AI really did so
3.
by practal 7d ago
Hmmh. I like motivated explanations, but, as acknowledged in the text, this is a subjective thing to measure. What is a great motivated explanation for Tao, might be hard to grasp for me. So I guess judging how well an explanation motivates
4.
The End of Mathematics(daniellitt.com)
33 points by practal 1mo ago|20 comments
5.
by practal 2mo 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
6.
by practal 2mo 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
7.
by practal 2mo 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?
8.
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?
9.
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
10.
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
11.
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
12.
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 :-)
13.
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,
14.
by practal 4mo 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/
15.
by practal 4mo 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.
16.
by practal 4mo 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
17.
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.
18.
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
19.
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:
20.
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
21.
We're excited to announce that AXLE is switching from Lean to Rocq(axle.axiommath.ai)
3 points by practal 6mo ago|1 comments
22.
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
23.
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
24.
by practal 7mo 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
25.
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.
26.
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
27.
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.
28.
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
29.
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
30.
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

More ›