Interesting bug: when pressing the text-to-speech button to hear my Swedish story read out loud, what I get is a pretty good rendition of the text read as if it were French.
Readit Newshejsansvejsan commented on DuoBook: Generate bilingual stories to learn any language duobook.co... · Posted by u/celltalk
Lean is a classical theory, I don't see how any intuitionistic theory can hope to possibly compete. A mathematician would laugh you out of the store if you tried to get them to used cubical Lean (Lean 2 by the way implemented HoTT ideas) and give up classical logic.
The HoTT people are doing good work and I don't doubt that automation can help with the _significant_ additional complexity of higher dimensional cubes, but that's not really all that would be missing.
Finally, if you can't claim Lean is good enough for all Mathematics then you can't claim it for any existing system or any system that doesn't take classical logic seriously (postulating an axiom doesn't count).
I'm confused by "postulating an axiom doesn't count". Are you aware that choice is an axiom in Lean?
https://github.com/leanprover-community/lean/blob/master/lib...
>Finally, if you can't claim Lean is good enough for all Mathematics then you can't claim it for any existing system or any system that doesn't take classical logic seriously (postulating an axiom doesn't count).
Correct me if I'm wrong (I may well be), but couldn't one work classically just by sticking to (-1)-truncated types ("mere prepositions") in a HOTT based system, for which LEM is true by default?
LEM for mere propositions is not "true by default", but it is consistent with univalence. So you can take it as an axiom.
It's easy to get a superficial understanding of the problem, and then very easy to subtly mis-understand it.
I've reviewed published papers by respectable people where they've made one of several easy mistakes:
* Be careful about how you encode your problem, it's easy to make it "too large", at which point your problem can be solved in P in the input size. For example, don't represent a sudoku as triples "x-pos,y-pos,value", where those 3 numbers are encoded in binary, because now if I give you a problem with only 2 filled in values, you can't take the solution as your 'certificate', as your input is about size 6 * log(n), but the solution will be n * n * log(n).
* It's also easy if you write your problem as a little language to accidentally make it impossible to check in P time.
* When proving a reduction (say turning SAT into a Sudoku, to prove Sudoku is NP-complete), it's (usually) easy to show how solutions map to solutions (so you show how the SAT instance's solution turns into a particular solution to the Sudoku). It's usually much harder, and easy to make mistakes, showing the Sudoku can't possible have any other solutions.