The Coq mailing list

[Camille Noûs <admin AT AnthropLOGIC.onmicrosoft.com>]

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
[3]: https://www.meetup.com/dubai-ai
[4]: https://editoReview.com
[5]: https://chat.openai.com/g/g-SBreMtSAF-editoreview-com
[6]: 
https://github.com/1337777/cartier/blob/master/Kosta_Dosen_polynomial_univalence.pdf