Lean4で小命題1件を形式化します

自然言語で書かれた小命題1件をLean4のコードにし、証明を検証します。既存のStd・mathlibの定義や補題で実装できる内容が対象です。購入前に定理文、仮定、結論、使用する定義とLeanの型を合意し、対応可否を確認します。 【10,000円の内容】 主命題1件と事前合意した補助命題について、.leanソース、版を固定した再現用プロジェクト、README、日本語による定理文と型の対応説明、ビルド・公理監査ログを納品します。ページ数・行数ではなく、定義や補題の準備、証明の難度で見積ります。必要情報と制作範囲を双方で確定してから10日が目安です。 【検収】 Lean版と依存のコミットを固定し、全納品Leanファイルをビルド対象に含め、lake build成功と各納品定理の#print axioms結果を確認します。許容公理はpropext・Classical.choice・Quot.soundのみ、または公理なし。sorry/admit、独自axiom、native評価由来の追加公理で証明を完成扱いにしません。型・仮定・結論を勝手に変更しません。実装不能と判明した場合はキャンセルを相談し、診断のみを満額の完成納品にしません。 【範囲】 未証明の研究定理、新規理論の大規模整備、論文全体の形式化、環境構築のみの依頼は対象外です。見本は集合版の商と像の対応をLean4.34.1・Stdのみで検証した制作例です。 【AI・権利・課題】 調査、コード案、説明に生成AIを使用し実検証します。資料を外部AIへ送る前に使用サービス・送信情報・目的を確認し同意を得ます。共有は権限のある必要最小限に限り、第三者ライセンスを保持します。評価対象の提出課題・試験・レポートの代作・完成答案は作成しません。 【訂正・質問】 納品後7日以内に連絡いただいた合意内容への不備・誤記・数学的誤りは無償訂正します。別枠で同期限内の質問を1往復まで受け付けます。新しい命題・版への変更は追加相談です。