Hacker News new | ask | show | jobs
by practal 777 days 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-order logic (set theory), simple type theory, or dependent type theory. You believe you will need to compromise, no matter which foundation you choose, so better just to pick your poison and get on with it. And I think pretty much everyone in the theorem proving space has that same opinion, so it is certainly a most reasonable opinion.

But I don't believe that the right logical foundation will make it harder to do mathematics on a computer than on paper, I think it will make it easier. In fact, I am pretty sure I have found that right logical foundation, Abstraction Logic [1]. I believe that it is indeed the best logical foundation, because it is simple and elegant (more so than any other foundation I am aware of), and it seems obvious that first-order logic, simple types, and dependent types are just special cases of it.

But a logic is not a working and proven system such as Lean + mathlib, so a lot of work needs to be done before my belief can be stated as a fact.

[1] http://abstractionlogic.com
1 comments
kevinbuzzard 777 days ago
I see! So I guess the proof of the pudding will be in the eating :-) Can you do algebraic geometry?
link
practal 777 days 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 Lean. If you had any difficulties formalising algebraic geometry in Lean caused by static types (for example that there are no subtypes), then that might be where AL could help.

Also, could you do category theory in general in AL? Again, I don't know category theory well enough to say. But categories can certainly be represented as mathematical objects, so I don't see why not.

Do you have a minimal example in mind where you encountered problems in Lean?

link