リンク先
応募フォームp2：文面案
以下は応募用の英文案です。計画は12か月・Book 3組を仮置きしています。チーム構成・担当、公開する成果の範囲は提出前に確認してください。
Project Title
Mathelia: AI Authorship of Self-Contained Mathematical Books
Categories
Early-stage research or prototypes
Tools or infrastructure experiments.
Project Summary
404 / 500 characters (including spaces and line breaks)
Mathelia is a web environment where people and AI write self-contained mathematical Books with definitions, theorems, and proofs. It addresses the difficulty of turning AI-generated mathematics into organized, inspectable work. We will improve AI authoring workflows, publish Books exploring different approaches to the same results, and build a small independent checker for Hyperion derivation records.
Key Objectives
697 / 1000 characters (including spaces and line breaks)
1. Improve the existing Mathelia prototype so that AI can write and revise self-contained Books, with explicit assumptions and feedback on proof steps.
2. Publish at least three pairs of Books that reach the same mathematical results through different definitions or proofs, with reproducible records of AI-assisted development.
3. Specify a bounded set of Hyperion inference rules and build a small independent checker for their derivation records. Clearly identify the external prover results and translation assumptions that remain trusted.
4. Release the project code, example Books, documentation, and evaluation cases publicly so others can reproduce results and test alternative approaches.
Implementation
841 / 1000 characters (including spaces and line breaks)
Proposed 12-month plan:
Months 1-3: Document the current authoring workflow and trust boundaries. Select mathematical examples and define evaluation criteria: successful Book checks, explicit dependencies, reproducible runs, and human review of exposition.
Months 4-6: Improve AI authoring feedback and produce three pairs of Books. Record revisions, failed proof attempts, and final checks to make the process inspectable.
Months 7-9: Fix a written specification for selected Hyperion rules and a derivation-record format. Implement a separate checker and test valid records, deliberately corrupted records, and known counterexamples.
Months 10-12: Run reproducible evaluations, invite external review, and publish code, Books, tests, and documentation. Report checker coverage and unresolved translation and prover dependencies separately.
Team Fit
469 / 500 characters (including spaces and line breaks)
The ATP Research Group is a small team in Japan developing Mathelia for automated theorem proving and formal mathematics. Our work includes a running web environment, mathematical Books, integration with external theorem provers, and Hyperion, our proof-step checking component. This existing prototype provides a practical base for the proposed authoring and verification work. We have begun technical exchanges with the Metamath community on independent verification.
Optional supplementary materials
Mathelia overview: https://atp-research.com/mathelia/about/
Human-oriented tutorials: https://atp-research.com/book_collection/?folder=0_tutorial_en
AI-oriented tutorials: https://atp-research.com/book_collection/?folder=0_tutorial_AI
補足資料は審査員には共有されず、AI for Mathチームのみが閲覧するというフォームの注記があります。主要な説明は上の回答内に含めています。
応募フォームp3：予算・期間の文面案
12か月計画。人件費は4人×月200ドル、サーバー代は月100ドル、AI利用料は月200ドルとして計算。合計は月1,100ドル×12か月＝13,200ドルです。サーバー・AIは機器購入ではなくサービス利用料なので、フォームでは Other Direct Costs に計上する案です。
Total Budget Requested
USD 13,200
Personnel
USD 9,600. Modest part-time stipends for four project contributors at USD 200 per person per month for 12 months (4 x USD 200 x 12). These stipends support contributions to Mathelia development, mathematical Book authoring and review, testing, and documentation; they are not full-time salaries.
Equipment
N/A. No hardware purchases are requested. Server hosting and AI service costs are listed under Other Direct Costs.
Travel
N/A. No travel funding is requested.
Other Direct Costs
USD 3,600. Server hosting: USD 100 per month for 12 months (USD 1,200), to host Mathelia and support project testing and reproducible evaluations. AI services: USD 200 per month for 12 months (USD 2,400), to support AI-assisted Book authoring, revision, and evaluation. Both costs directly support project execution.
Indirect Costs
N/A. No indirect costs are requested (USD 0).
Estimated project duration
12 months
フォームの注意：Submit後は応募内容を編集できません。