Viva, Atticus! > Fui um dos membros "fundadores" dessa organização e gostaria de poder > responder quaisquer perguntas que vocês tiverem a respeito. Eu me oponho > fortemente ao uso atual da IA na pesquisa matemática, e acho que, se não > houver reformas fortes com respeito a publicação, revistas, padrões éticos na > área, etc, o jeito no qual muitos matemáticos (incluindo alguns dos > matemáticos mais prominentes) estão usando a IA vai destruir a nossa > comunidade. > > Se vocês tiverem perguntas, por favor, me perguntem; eu tô totalmente > disposto a explicar o propósito da organização mais.
Tenho uma pergunta: seria este o tipo de "parceria" contra a qual a AHM se posiciona? %%% https://arxiv.org/html/2609.05669v1#intelligence:~:text=1%2E2%2E%20Use%20of%20artificial%20intelligence 1.2. Use of artificial intelligence To complete this work, we built our own experimental proof-development environment primarily around OpenAI’s Codex, with occasional use of Anthropic’s Claude Code. The evolving body of mathematical information which is required to discover and construct a long mathematical proof—not merely the streamlined argument presented a posteriori in the finished paper—spans many model context windows. Our environment therefore served as an external memory and coordination layer, as well as the interface through which we interacted with the models and directed the development of the proof. It decomposed our evolving proof into over a hundred blocks, distributed across auxiliary files, and a “master” file assembling them. Models could operate on individual blocks largely independently, using only the locally relevant context and dependencies. An HTML-based visualizer displayed the proof’s structure and current review status of each block, while Python tools tracked their dependencies and propagated status changes downstream. This setup allowed us to retain full mathematical control while using frontier models to draft and check technical passages. It also allowed us to quickly propagate changes in the proof architecture through the entire argument. When, for example, we changed an early definition or lemma, the models carried out routine downstream revisions and identified any genuinely new mathematical obstacles that arose. This allowed us to fully focus on the genuine blockers at each moment. [...] This is a factual account of the division of labor in this project, not a general claim about the limits of the models. We record it not only for transparency, but also because it illustrates a mode of AI-assisted mathematics that is obscured by a focus on one-shot theorem proving. In this project, the strategy and key computations remained human-generated, while AI substantially accelerated their local completion, systematic criticism, revision, and propagation. As the models and the surrounding workflows improve, the division of labor described here may also change; this statement records the balance in the present project. We realize, however, that the mathematics to come may emerge from a different balance between human and machine. %%% Tudo de bom, João Marcos -- https://sites.google.com/site/sequiturquodlibet/ -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <[email protected]> --- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para ver esta conversa, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LiTt%2BhbGa00jniaC2AbRE5h28e3dbL9Yv5eQacCdsvzcg%40mail.gmail.com.
