Post #2636087
2026-05-05 20:29 UTC
@JacquesC2@types.pl
Happy to disagree.
TypeTopology follows the flow of ideas, given that its main purpose is to be a giant blackboard to produce new mathematics rather than record already-existing mathematics.
Proof-engineering tools should be used to make them into encyclopaedic format in the sense you want, not the other way round.
Sadly, such tools don't exist, but I think they are perfectly possible (without the need of any AI nonsense).
(And you comparison of LaTeX and PDF are not related to this discussion, as far as I can see. In fact, LaTeX contains more logical information than PDF, which, of course, trained people can recognize from the PDF.)
@egbertrijke@mathstodon.xyz @gallais@mamot.fr
Replies (1)
-
@JacquesC2@types.pl 2026-05-05 20:40
@MartinEscardo@mathstodon.xyz Hopefully we'll have occasion to meet in person in a setting where we can discuss all of this at leisure. I think the outcome of such a discussion is likely to be: 1) an "oh, I see" from you, 2) a continued "happy to disagree"! I liken it to (say) the main ocaml and haskell developers meeting to compare notes. They learn a lot from each other but still leave with some core opinions unchanged. [I have personally witnessed this.] And yet each side has truly learned something. @egbertrijke@mathstodon.xyz @gallais@mamot.fr