Post #2636086

2026-05-05 12:09 UTC

@MartinEscardo@mathstodon.xyz Note that I also like story-like narrative. My main points remain: the needs of libraries and narrative are very different (and thus need different solutions)being bound to 'files' as a unit of source is a bad idea When you read a paper, you read the PDF, not the LaTeX source, right? Why should Agda be any different? @egbertrijke@mathstodon.xyz @gallais@mamot.fr

Replies (1)

@MartinEscardo@mathstodon.xyz 2026-05-05 20:29

@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

Open ##2636087