Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

I see! So I guess the proof of the pudding will be in the eating :-) Can you do algebraic geometry?


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?




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: