汎用LLM・AI開発⭐ リポ 2品質スコア 64/100

lean4-prove

Retrieval-augmented Lean4証明生成と自己改善ラボ機能。DeepSeek-Prover V1+V2から94k件以上の事例を検索し、ハイブリッド検索（BM25+セマンティック+グラフ）を活用します。Claude経由で生成し、lean-interact（20並列処理）でコンパイルでき、失敗時は自動的に再試行します。ラボモードでは、HFデータセット取り込み、並列コンパイル、英語↔Lean4の自動形式化、コンパイラ報酬を用いたGRPO学習、収束ループ、および対抗的ベンチマーク測定が可能です。

description の原文を見る

Retrieval-augmented Lean4 proof generation with self-improving lab. Queries 94k+ exemplars from DeepSeek-Prover V1+V2, uses hybrid search (BM25 + semantic + graph), generates via Claude, compiles via lean-interact (20 parallel silos), retries on failure. Lab mode: HF dataset ingestion, parallel compilation, English↔Lean4 autoformalization, GRPO training with compiler rewards, convergence loop, and adversarial benchmarking.

SKILL.md 本文

注意: このスキルのライセンスは ライセンス未確認 です。本サイトでは本文プレビューのみを表示しています。利用前に GitHub の原本でライセンス条件をご確認ください。

停止。このSKILL.MDをすべて読んだ後、エンドポイントを呼び出してください。

lean4-prove

エンジニアリング要件のためのレトリーバル拡張Lean4証明生成。DeepSeek-Prover V1+V2から94,000以上の証明済み定理を使用して、ハイブリッド検索(BM25+セマンティック+グラフトラバーサル)を通じた証明合成をガイドします。

アーキテクチャ(2026-03-29更新)

要件 + タクティック + ペルソナ
        │
        ▼
┌───────────────────────────┐
│ 1. 類似証明を回想          │  ← ArangoDB上のハイブリッド検索
│    94k+の事例から         │     (BM25+セマンティック+グラフ)
└───────────────────────────┘
        │
        ▼
┌───────────────────────────┐
│ 2. サポートパックを構築     │
│    - 検証済みインポート    │
│    - タクティックパターン  │
│    - 類似証明            │
└───────────────────────────┘
        │
        ▼
┌─

...

全文を GitHub の原本で見る →リポジトリ

詳細情報

作者: grahama1970
リポジトリ: grahama1970/agent-skills
ライセンス: 不明
最終更新: 2026/5/11

GitHubで原本を見る →フィードバックを送る

Source: https://github.com/grahama1970/agent-skills / ライセンス: 未指定