AI, Math, Open Source Funding Opportunity
Patrick Masson
Applicable?
Please
forward this funding alert from our partners at Renaissance
Philanthropy to relevant faculty, researchers and programs.
For more information, contact: Megan Scarborough, UT
Foundation Relations me...@mail.utexas.edu.
AI for Math Fund Details
- Individual grants: up to $1M for up to 24 months of work on open-source projects and research
- Open to individuals and teams worldwide focused on Datasets, Production Grade Software Tools, Field Building, Breakthrough Ideas (see details below)
- Read more in the Request for Proposals and the Proposal Instructions.
-
Application Deadlines
- Brief web form: January 10, 2025
- Proposal: March 3, 2025
- Decisions: April 7-11, 2025
-
Application Process
- Submit this simple application.
- Selected applicants submit a full proposal.
- Selected applicants will have an interview where their proposal is discussed in depth.
-
Advisors
Click here for a list of AI for Math Fund advisors.
-
Eligibility
Applicants should have a strong background in formal verification, AI, proof assistants, or mathematics.
-
IP and Data Sharing
All code, datasets, and research outputs must be open-access, with preprints shared in public repositories.
Strategy
An increasing number of researchers, including some of the world’s leading mathematicians, believe that the mathematics of the future will be discovered, and studied, with the help of AI tools. The AI for Math Fund is dedicated to creating AI technologies that are valuable for mathematicians and expanding their use in the global mathematical community.
Through an RFP and open call for applications, the AI for Math Fund will support projects across four tracks: Open Source Tools, Transformative Datasets, Breakthroughs, and Field Building.
Projects may be led by applicants from academic institutions,
commercial organizations, or independent projects, so long as
all work is open-source and shared publicly, and is separate
from the business-as-usual activities of any for-profit
company. Typical applicants will have strong track records of
achievement in formal verification, AI, and related fields.
1. Production Grade Software Tools
The AI for Math Fund will support projects that develop open-source, production-quality software tools in the intersection of AI and mathematics, such as:
- AI-based autoformalization tools for translating natural-language mathematics into the formalisms of proof assistants
- AI-based auto-informalization tools for translating proof-assistant proofs into interpretable natural-language mathematics
- AI-based models for suggesting tactics/steps or relevant concepts to the user of a proof assistant, or for generating entire proofs
- Infrastructure to connect proof assistants with computer algebra systems, calculus, and PDEs
- A large-scale, AI-enhanced distributed collaboration platform for mathematicians
2. Datasets
The AI for Math Fund will support projects to produce open-source datasets for training AI models, such as:
- Datasets of formalized theorems and proofs in a proof assistant
- Datasets that would advance AI for theorem proving as applied to program verification and secure code generation
- Datasets of (natural-language) mathematical problems, theorems, proofs, exposition, etc.
- Benchmarks and training environments associated with datasets and model tasks (autoformalization, premise selection, tactic or proof generation, etc.)
3. Field Building
The AI for Math Fund will support projects that grow the field of AI for math, such as:
- Textbooks
- Courses
- Documentation and support for proof assistants, and interfaces/APIs to integrate with AI tools
4. Breakthrough Ideas
The AI for Math Fund will support some high-risk, high-return ideas for applying AI to fundamental mathematics and applications, such as:
- Expected difficulty estimation (of sub-problems of a proof)
- Novel mathematical implications of proofs formalized type-theoretically
- Formalization of proof complexity in proof assistants
For more information, and if you intend to apply, please
contact: Megan Scarborough, UT Foundation Relations
me...@mail.utexas.edu.
Patrick Masson
Thank you Shoji. What do others on this list (and others in the
Sakai community) think?
Let me share this with Josh Baron, Apereo's Development Director, for his thoughts.
Patrick
Hi Patrick, Just an idea:-) Title: An Open Source LTI Tool for LMS: AI-Enhanced Handwritten Math Assignment Solutions Abstract: We propose a solution for managing handwritten math assignments by integrating Open Source Learning Management Systems (LMS) with the 1EdTech Learning Tool Interoperability (LTI) standard, powered by advanced Deep Learning technologies. Our team is composed of international researchers and practitioners with expertise in mathematics, deep learning, open source development, and open standards, representing institutions such as the University of Michigan, University of British Columbia, Kyoto University, Nagoya University, and the Apereo Foundation. Building upon the AI-driven Kamirepo platform, we will develop an enhanced version tailored for handwritten math assignments. This solution will be implemented and tested in real-world mathematics courses at the University of British Columbia, Kyoto University, and Nagoya University to evaluate its effectiveness and efficiency. UBC Math Plom: A free solution for paperless open marking https://2023.fossy.us/schedule/presentation/150/index.html Nagoya U ITC and Math Kamirepo: Automatic Student Identification to Handle Handwritten Assignments on LMS https://researchmap.jp/ddeguchi/published_papers/35836310 Kyoto U Math Professor Shishikura who was a collaborator with Shoji https://en.wikipedia.org/wiki/Mitsuhiro_Shishikura UMich School of Informatics Chuck Shoji
. AI for Math Fund Details • Individual grants: up to $1M for up to 24 months of work on open-source projects and research • Open to individuals and teams worldwide focused on Datasets, Production Grade Software Tools, Field Building, Breakthrough Ideas (see details below) • Read more in the Request for Proposals and the Proposal Instructions. - Application Deadlines • Brief web form: January 10, 2025 • Proposal: March 3, 2025 • Decisions: April 7-11, 2025 - Application Process • Submit this simple application. • Selected applicants submit a full proposal. • Selected applicants will have an interview where their proposal is discussed in depth. - Advisors Click here for a list of AI for Math Fund advisors. - Eligibility Applicants should have a strong background in formal verification, AI, proof assistants, or mathematics. - IP and Data Sharing All code, datasets, and research outputs must be open-access, with preprints shared in public repositories. Strategy An increasing number of researchers, including some of the world’s leading mathematicians, believe that the mathematics of the future will be discovered, and studied, with the help of AI tools. The AI for Math Fund is dedicated to creating AI technologies that are valuable for mathematicians and expanding their use in the global mathematical community. Through an RFP and open call for applications, the AI for Math Fund will support projects across four tracks: Open Source Tools, Transformative Datasets, Breakthroughs, and Field Building. Projects may be led by applicants from academic institutions, commercial organizations, or independent projects, so long as all work is open-source and shared publicly, and is separate from the business-as-usual activities of any for-profit company. Typical applicants will have strong track records of achievement in formal verification, AI, and related fields. 1. Production Grade Software Tools The AI for Math Fund will support projects that develop open-source, production-quality software tools in the intersection of AI and mathematics, such as: • AI-based autoformalization tools for translating natural-language mathematics into the formalisms of proof assistants • AI-based auto-informalization tools for translating proof-assistant proofs into interpretable natural-language mathematics • AI-based models for suggesting tactics/steps or relevant concepts to the user of a proof assistant, or for generating entire proofs • Infrastructure to connect proof assistants with computer algebra systems, calculus, and PDEs • A large-scale, AI-enhanced distributed collaboration platform for mathematicians 2. Datasets The AI for Math Fund will support projects to produce open-source datasets for training AI models, such as: • Datasets of formalized theorems and proofs in a proof assistant • Datasets that would advance AI for theorem proving as applied to program verification and secure code generation • Datasets of (natural-language) mathematical problems, theorems, proofs, exposition, etc. • Benchmarks and training environments associated with datasets and model tasks (autoformalization, premise selection, tactic or proof generation, etc.) 3. Field Building The AI for Math Fund will support projects that grow the field of AI for math, such as: • Textbooks • Courses • Documentation and support for proof assistants, and interfaces/APIs to integrate with AI tools 4. Breakthrough Ideas The AI for Math Fund will support some high-risk, high-return ideas for applying AI to fundamental mathematics and applications, such as: • Expected difficulty estimation (of sub-problems of a proof) • Novel mathematical implications of proofs formalized type-theoretically • Formalization of proof complexity in proof assistants For more information, and if you intend to apply, please contact: Megan Scarborough, UT Foundation Relatio...@mail.utexas.edu. -- You received this message because you are subscribed to the Google Groups "Sakai PMC" group. To unsubscribe from this group and stop receiving emails from it, send an email to sakai-pmc+...@apereo.org. To view this discussion visit https://groups.google.com/a/apereo.org/d/msgid/sakai-pmc/c7dd4be2-4efb-4dc7-9bb8-5fc608e841da%40apereo.org.
Patrick Masson
Executive Director
Apereo Foundation
9450 SW Gemini Dr PMB 98572
Beaverton, OR 97008-7105
Mobile: +1 (970) 4-MASSON
Calendar: Book a call
Charles Severance
Patrick,
I think that Shoji's approach to do it through an independent LTI tool as a separate open source project is a good idea.
At this point, we are pretty far away from adding "AI stuff" to the core Sakai LMS. Some of our work improving Sakai's Archive / Export process wll make it more straightforward to take the content of a Sakai course and extract it - and then feed it into some kind of AI system - but we probably won't be adding that "AI system" into Sakai core per se any time soon.
Separately - this is a really friendly call for proposals. Makes me kind of wish I was in the space.
/Chuck
To view this discussion visit https://groups.google.com/a/apereo.org/d/msgid/sakai-pmc/9502fad6-7755-4b78-badc-1b633411f78d%40apereo.org.