Email Gateway (Jul 14 2025 at 12:48): Email Gateway (Jul 14 2025 at 12:48):From: Christopher Mary <christopher.mary@outlook.com>
Dear Larry Paulson,
Dear Isabelle list,
Thank you for the report and raw data. I would also like to mimick Larry and share a report of my such experiments, for the interest of the Isabelle community who may not be up to date to the latest weekly non-expected benefits of AI:
The topic of computational methods for categories, ω-categories, sheaves and schemes dates back to authors such as David Rydeheard, Tatsuya Hagino, and Kosta Dosen.
A key challenge, even for those specialists expert-authors, has always been how to quickly scaffold and prototype a specialist computer experiment, without literally becoming software engineers pros themselves.
I can share my experience report that, with tools such as Gemini 2.5 Pro AI released last month, you don't need to be a "pro" to bring your specialists math synthesized ideas into usable prototypes for further experiment and theoretical discovery:
« Emdash: A Dependently Typed Logical Framework for Computational Synthetic Category Theory and Functorial Elaboration »
https://github.com/hotdocx/emdash/blob/main/docs/emdash.pdf
emdash is a new functorial programming language for ω-categories and schemes implemented in Typescript. emdash features a bidirectional type checker with higher-order unification-based hole solving for interactive proof, definitional equality via βδι-reduction (including user-supplied rewrite rules and unification rules), Higher-Order Abstract Syntax (HOAS) for binders, and features a new "functorial elaboration" paradigm where coherence laws (e.g., functoriality, naturality) for kernel constructors are definitionally verified via Kosta Dosen techniques. emdash was 99% generated by Gemini 2.5 Pro based on my deep specification of the emdash kernel written in the Lambdapi proof assistant:
https://github.com/1337777/cartier/blob/master/cartierSolution18.lp
A one-liner description of this spec is as follows: for the functoriality rule (F b) ∘> (F a) ↪ F (b ∘> a) it is clear that the size of the composition term (b ∘> a) in the RHS is smaller/decreasing; but for the naturality rule (ϵ._X) ∘> (G a) ↪ (F a) _∘> (ϵ._Y) it is not clear how to make the computation progress towards a smaller RHS, and the key insight by Kosta Dosen is that the RHS _∘> is actually a Yoneda/hom action/transport which is syntactically distinct than (but semantically equivalent to) the usual composition ∘> ... Moreover there is strong evidence that similar insights can be extended to computer implementations for simplicial-cubical ω-categories, sheaves and schemes (but I will try hard to stay agreeable, and stop here to what everyone can agree to, lol)
You can try and experiment with emdash functorial programming within the hotdocx publisher web app:
https://hotdocx.github.io/#/hdx/25188CHRI27000
À bientôt,
Christopher Mary
P.S. hotdocx, the hottest fastest calendared marketplace publisher, was also 99% generated by Gemini 2.5 AI and is an open-source GitHub sponsored project: https://github.com/sponsors/hotdocx
Last updated: Jul 26 2025 at 12:43 UTC