A Renaissance Philanthropy e os mercados XTX anunciou o lançamento do Fundo AI para Matemáticaum novo programa de subsídios que apoia projetos que aplicam IA e aprendizado de máquina à matemática, com foco na prova automatizada de teoremas, com um financiamento inicial de US$ 9,2 milhões. As categorias de financiamento de projetos e exemplos de projetos nessas categorias são:
1. Ferramentas de software program de nível de produção
Ferramentas de autoformalização baseadas em IA para traduzir matemática de linguagem pure em formalismos de assistentes de prova
Ferramentas de autoinformalização baseadas em IA para traduzir provas de assistente de prova em matemática interpretável em linguagem pure
Modelos baseados em IA para sugerir táticas/etapas ou conceitos relevantes ao usuário de um assistente de prova ou para gerar provas completas
Infraestrutura para conectar assistentes de prova com sistemas de álgebra computacional, cálculo e PDEs
Uma plataforma de colaboração distribuída em grande escala e aprimorada por IA para matemáticos
2. Conjuntos de dados
Conjuntos de dados de teoremas e provas formalizados em um assistente de prova
Conjuntos de dados que avançariam a IA para prova de teoremas aplicados à verificação de programas e geração segura de código
Conjuntos de dados de problemas matemáticos (em linguagem pure), teoremas, provas, exposição, and many others.
Benchmarks e ambientes de treinamento associados a conjuntos de dados e tarefas de modelo (autoformalização, seleção de premissas, geração de táticas ou provas, and many others.)
3. Construção de campo
Livros didáticos
Cursos
Documentação e suporte para assistentes de prova e interfaces/APIs para integração com ferramentas de IA
4. Ideias inovadoras
Estimativa de dificuldade esperada (de subproblemas de uma prova)
Novas implicações matemáticas de provas formalizadas na teoria do tipo
Formalização da complexidade da prova em assistentes de prova
