Re: [CFP] Dosen's polynomial functorial programming & AI @UAE NYU 17th Jan — Re: [categories] Outreach Panel

Re: [CFP] Dosen's polynomial functorial programming & AI @UAE NYU 17th Jan — Re: [categories] Outreach Panel

[Camille Noûs]

[-- Attachment #1: Type: text/plain, Size: 6515 bytes --]

David السلام عليكم

[1]: https://github.com/1337777/cartier/blob/master/cartierSolution15.lp

Indeed, AI assistants extended by proof assistants could be used for political outreach to crowdsource the editorial review of research articles such as this Kosta Dosen's univalent polynomial [functorial programming][1]. I confess I stole your ideas from your `polytt` github and rebranded it so to get a tribalist attribution to me; at least it is not robbery like at CT2023, lol...

## AI IN UAE

This Wednesday 17th January 2024 in Abu Dhabi @ NYUAD has this `The AI Mathematician` (CQTS M-theory) [conference][2] by Yang-Hui He.

And Saturdays in Dubai @ DIFC has this `DubAI AI` [meetup][3] with 1000+ participants, sponsored by editoReview.com a new methodology platform for the editorial review of the AI intelligence at the interface of research articles and tools/plugins API.

## AI-PROOF-ASSISTANTS

Last week, Blaauwbroek-Pestun announced some form of AI-proof-assistant: the Coq Tactician's API, whose goal (should) include how to interface AI assistants LLM with (“dynamic chaining” of) external agents/tools/plugins API such as proof-assistants (or weather sensors).

In today's digital landscape, a developer writing an AI prompt that orchestrates an interface among various tools/plugins API is akin to an academic author writing a scientific article: therefore, the ability-or-not of AI-proof-assistants to intelligently use or search within an interfacing prompt or article is a new form of editorial review; and is prologue to any eventual (expert) peer “reviewing” (i.e., coauthoring) of a byproduct article that cites the original article.

This methodology is being implemented at [editoReview.com][4] via Microsoft Copilot Studio and via the OpenAI [ChatGPT GPT store][5], and is government-auditable thanks to its Microsoft SharePoint back-end. The user types a prompt such as `Start the editorial review of the arXiv article “Functorial Aggregation” by David Spivak` (or any Bing-indexed article in HAL, F1000, OSF, viXra, etc.), then the AI responds with a basic question to qualify the user as having paid attention to the literal article, and finally the user challenges the AI with questions/searches for complex (i.e. “natural”) knowledge that should be AI-inferable from the literal content of the article if this article is indeed “sensible” in the context of the training literature.

## MICHAEL BARR ON EDITING

Yesterday, Michael Barr wrote some historical stories, in the category theory mailing list, hinting at some challenges in academic publishing such as editorial reviewing, peer reviewing, refereeing, and its non-reliability. They wrote:

« And it was duly published. But if the editor hadn't been a friend? I don't know. »
« around 1990, Bob sent me an email asking my opinion about an online free journal on category theory. ... The papers would have to use TeX which most mathematicians were not using, although many were learning. There were no browsers and the papers would have to be distributed via ftp »

The lesson here is that regardless that the technology may not be ready yet, the essence of the editoReview methodology remains valid: because many researchers are already using AI assistants to “search within” research articles, it is feasible to do so through a tool such as editoReview which _keep records_ of these crowdsourced interactions in the format of `whether yes-or-no the AI-search result satisfies the (qualified) user's expectation`. There is an analogy in law: how the question is framed and qualified, and the creation of a legal record of the data, are more determinative than the (impotent) argumentation itself...

## CALL FOR PAPERS/PROMPTS

Following up from my talk last week at TFP 2024, here is an updated [Call for Papers/Prompts][6] for an upcoming workshop, collocated “around” ACT/CT 2024 and edited by editoReview.com, on implementing Kosta Dosen's functorial programming with higher groupoidal symmetry (homotopy types, univalent higher categories) and with polynomial algebra (polynomial monads, databases, effects, and dynamics).

The basis for this implementation is the ideas and techniques from Kosta Dosen’s book « Cut-elimination in categories » (1999), which essentially is about the substructural logic of category theory, in particular how some good substructural formulation of the Yoneda lemma allows for computation and automatic-decidability of categorial equations. Polynomials truly arise from the dualities in the many ways to store the data info of a category, i.e., the substructural logic of category theory, whereas Univalence is what would unify Voevodsky's homotopy type theory (symmetry) along Dosen's functorial programming.

For concreteness, here is some example Lambdapi code which shows how to store the underlying profunctor data (over a category of elements) for the composition of two polynomial modules:

constant symbol pmod_cov : Π [A : cat] (PA : mod Terminal_cat A) (B : cat), TYPE;
constant symbol ⊲pmod_cov : Π [A B C : cat] [PA : mod Terminal_cat A] (R : pmod_cov PA B), Π [PB : mod Terminal_cat B] (S : pmod_cov PB C), pmod_cov ((PB ⇐pmod_cov R) ×pmod (Proj_pmod_cov PA)) C;

-----

[2]: https://ncatlab.org/nlab/show/M-Theory+and+Mathematics<https://protect-au.mimecast.com/s/7ohECgZ05Jf2NDLyCEZL6F?domain=ncatlab.org>
[3]: https://www.meetup.com/dubai-ai<https://protect-au.mimecast.com/s/Ser1CjZ12RfqAV7munol9-?domain=meetup.com>
[4]: https://editoReview.com<https://protect-au.mimecast.com/s/7RQPCk815RCQ4PMBsk_Ms3?domain=editoreview.com>
[5]: https://chat.openai.com/g/g-SBreMtSAF-editoreview-com<https://protect-au.mimecast.com/s/-n5oClx1OYUZkjBEsgkCY8?domain=chat.openai.com>
[6]: https://github.com/1337777/cartier/blob/master/Kosta_Dosen_polynomial_univalence.pdf



You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message.

View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Learn more about Microsoft 365 Groups<https://aka.ms/o365g>


[-- Attachment #2: Type: text/html, Size: 8591 bytes --]