Repository navigation
Expand file tree
/
Copy pathSHA256SUMS
More file actions
98 lines (98 loc) · 9.19 KB
/
Copy pathSHA256SUMS
File metadata and controls
98 lines (98 loc) · 9.19 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
7403903e9ad1cf4c4bad9824c17c39e2e2f0dffa26e967d581129263f0edb059 .gitignore
4a5e85cede3cdf2421034ae501372a5eb2e9b96eed55cc059b47a8b7803a5857 CONTENTS.md
929056634ad921f558b878ed78c3bd3d51298368140e58ccbbb40dc9688c01d4 GUIDE.zh-CN.md
c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4 LICENSE
60b85087aeb3221a5f30d67ee42858a6c4744eb03f5c30cc5d41b52f294e2681 LICENSE-MIT
f0fb0313f3d79204d6c4f98fd3ab1e7887d9b4a753cad32a8f4f08f2d58f440e NOTICE
20901d40c7cce85fc2ea8e927608a3f453ba2359b7b179257f6022ca7009e81b PAPER_SETTINGS.md
c45c47019a130ed62bf8db5f8c7165cf7b61b272cd77f320b8980bcc0065b507 README.md
4ddfd6d42b29807f30cee2805dc134a1c4d8470a4e07cdc31cddff177b4adf56 REPRODUCING.md
a06f36cfbbdb8f04b7c7ba9f62c2174df31fe6cb58e852799cf8c8051d135467 THIRD_PARTY_NOTICES.md
c97c6d6820350cd744491d9865c88b4ab63c3e2a7e48d04eae6dca7c6370740c assets.lock.json
909622e0e32f5f26405e08865d07ba4f9156de4adc261806184efb7a43644db9 benchmark/FATE-H.LICENSE
b3557e31bd4d02c59b392f972d32cae992ec32a894c81e1d0515b86eb066fd98 benchmark/FATE-H.jsonl
3cb69b0082e6712aa34292cd2014a5b4f2fbdccd534af05aa6b52ec1b18189b7 benchmark/LeanIMO.LICENSE
6650004fac2fc246692508a27a0fd35d3bd22c74d3a24d369210d97b70a0dfa7 benchmark/LeanIMO.csv
91a52d4998e81663effcf94cfe72908054577a2a9c16ddd7b32bc61657f4f9a7 benchmark/MathlibMPR.json
4c53d9edbe5dcbcf84d9e687f0a292b8dcc6d162c24a71abc84a0d3a0655f4cc benchmark/MathlibMPR_Prop_ids.txt
0ce093ebb9da90c046d10b4e50a901edd8237a5aef357df1a3e08f5f5c1a1294 benchmark/MathlibQR.json
a57a0048bdd14c5a9f5815a51846163b9c3fd059fe8ea529651dc6af02a35962 benchmark/MathlibQR_shared171.json
356bfe20c5d718fd628c091ee6e81642c277c382d87fedab51bf2adf21a30ad6 config.example.yaml
4f38d1eb33babec0270cdc1a5900f07aed97cd47b0ce3bf2768b02fd5ab54bf2 config.yaml
db803edc185a493c0eea73e510d65112e1dc1a043518e774ce184d0d09fd7f71 configs/proving.yaml
146fb10f48e9585da08da1aa5140cbf0500ec89b51e369c5a3eea7948be5cf2c configs/reasoning_claude_graph.yaml
e0533be15b595c5e2f29d1f91d6c10d5368a8f88e25f545ad3bf1b46d3c48a51 configs/reasoning_claude_standard.yaml
4e51d36c96c3dee22369f8d4ccaaa00919f22e279fa71a55928c1ca1ba0f7a7a configs/reasoning_gemini_graph.yaml
79267e3e765ade4e4776a0069c92350d02e88c43e1073390da2ee9717d51f22a configs/reasoning_gemini_standard.yaml
dd3e8852527bf56bc066a28b84db60315a06488be6fb6d00a3ea21df231ff66d pyproject.toml
ca2003ea15e268d9044a50b0ce0776afd22c9c4a9a41f9b1210f222cbd8b522c requirements-test.txt
f64cbfd180fcaa48608c2b5c7a72d83400e09cfa7b233750db5c7042ca799c28 requirements.txt
40e1549c074f3cc2a1ab68cf1f2c26616477136b0629f743775284a0f8d3daf8 scripts/analyze_proving.py
82e139099036490bd75be3dcb9b0741cf91e3f6ad00d3653a6a384cb0a47e813 scripts/prepare_dependencies.py
d1362553801804dffb372c948ddaf0187ff37c089e8320e36941f17848a0c00e scripts/reproduce_mathlibqr.py
12bdfe1cd61f4d6577f246ef3b6864565789f937781308774a8319c008dea0a6 scripts/reproduce_premise_costed.py
e6a770ff1a256a64c0a42bf9ada76e3f4aee3234420ed2df19f01a673a99ed7b scripts/reproduce_proving.py
4b0dccd5a47dd79338a18d356088e87fc67af4b4dcd88732d8c53976514e261a scripts/serve.sh
6ebbdb08df052464b422d4487e9ecf0c14ce42f363523a08da4ff674c0cc722d scripts/smoke_graph.py
9dec771938d32e6f64ea95590e589f7b0e2ebf920e7602b99e0e33f947071e68 src/leansearchv2/__init__.py
afe90c4eb0318770b4050fbc0f83fc9aa1405c19546f10573d6fb461d8f9a1b1 src/leansearchv2/config.py
e3a406ed43c6f82e07768f757aca04b572ac4dc8032843c664dda29b0cd0b918 src/leansearchv2/corpus/__init__.py
16d51ca95d986a9fc259c635f8495f3578b807f39d2fb9dc1b480d501e52cadb src/leansearchv2/corpus/jixia_extract.py
c9358e299a8b4ce3c5c89053e8668138e7745012b391868d36ea4ef66bd2b68b src/leansearchv2/corpus/merge_to_jsonl.py
ca7a925d2206b0b7c4ee55b20a950b3856954bc7d3a81fd540be93fd66a8b01a src/leansearchv2/eval/__init__.py
e338975a5f5e98f17dc93915b3f68f8ab384d179f2b4ec2300f026c03704f827 src/leansearchv2/eval/premise_metrics.py
07a9a86e16706cbad29d1586be01ead01c0976f6f09b17e1d37d783a883d9ece src/leansearchv2/eval/search_metrics.py
6662769b3ff1ef8e1f4f229d0f7bd2b8b856b316dd8a3eb4c05867df0dfdcb89 src/leansearchv2/gemini_client.py
20b437dd9353e5776c05c2d621c09589901d64c7412d704c7cf31d7b9980175e src/leansearchv2/graph/__init__.py
b9e829a0a1a22dde8505aa1ffab019361cfa51920ea0811053292dea45ce77b1 src/leansearchv2/graph/artifact.py
f3322883e2a2881a22da960576cdc5cffaa5ae21d3adff929b2fc34e3f0accb6 src/leansearchv2/graph/augment.py
b9d97b34beb7f5188a7e76ef7e09f10736c50eea3b76b08fedd56972c0ee3fb4 src/leansearchv2/graph/build.py
34a24e72b68e732579353ed789ae7e509770a874e73c194eb00a33cdd5ccc54e src/leansearchv2/graph/config.py
bd36738c0b9273193782d745e7b6df7909cc358e90aa0a8df445056f39b2f1ac src/leansearchv2/graph/ppr.py
cecacb57d8eebf8dd1e00d24e221c8d00044c2dc220ac1dd26da2826201a548c src/leansearchv2/graph/schema_inspection.py
907a5454a22ff081a5a40a358f5e41c1ea07be54f83960aa5dd0ff916bc82b58 src/leansearchv2/imo_eval/__init__.py
42a0f35fd09cee622298c5af0c89c407804abcea261d078193fe95415daff31d src/leansearchv2/imo_eval/benchmark.py
19626b21f3b9bc35e0f39b2c16ec3e6e19f5e1792503634170c9c2d49f0e9d32 src/leansearchv2/imo_eval/diagnostics.py
f6b113818c581557ec1f3e7f7db1bdf55ad186e9c6c748afc11aae77806be4e4 src/leansearchv2/imo_eval/failure_memory.py
16af483668c9f071e17d5363109b415803ac1c84072b3025d9cfb6c8cb234725 src/leansearchv2/imo_eval/failure_state.py
0b30c41759979534c9c8ce6e171fee47099a9e48d761f9982a08fa6e28ff6878 src/leansearchv2/imo_eval/problem.py
9e9a1769a20381fa25c81464be140a116cde9711eef1f8cb1b32e3b16e15a198 src/leansearchv2/imo_eval/source_utils.py
1275250859bf95e0aa5da3a8debc6c8d81acce267f92e5686a25166c6b6ee521 src/leansearchv2/llm.py
e8410f2c5714999e8f1a13c32f822d8280f759af85bc2340173f3d1a737e9682 src/leansearchv2/pipeline.py
81b559a65ffc2fafb07de3c15ce8a6224b9e62aae2340ad4b80c00039bf9cfce src/leansearchv2/prove/__init__.py
4c3c8d510c76ad65d786eb8aec9064722bd57103a4f7fae0ae88e216e3e16a1c src/leansearchv2/prove/budget.py
f36f28e404d19e0a55428fe5e5f4a95769551e945bc074eb93787754940faf04 src/leansearchv2/prove/integrity.py
e5efeeb13767abd9a7c797916fd1030376b33bba77fb95896fa23f4e99771e82 src/leansearchv2/prove/prompts.py
5d26c700839158f1ff15c53d27acdc2b60538e4001fce4197504904193fa445b src/leansearchv2/prove/run.py
a98ccb071aef97f948c0e925f678791b22425ba253d39fe1c328f08abe8cd5bb src/leansearchv2/prove/telemetry.py
ad1e2dcd16505c543bb4f66a1746bb9d8dd3685236a08c9be2780f739b4a2aec src/leansearchv2/prove/verifier.py
0064e338fc442f91b5c21e78c0f96324ff37776827ef68d46452e06d2f6a4c8f src/leansearchv2/reasoning/__init__.py
3f3957b6f17a1fcc4bbe4fce3acaa62addf66bf8ec4fce0a9aee17a6c1bbe9da src/leansearchv2/reasoning/decompose.py
cd5acce3bba4fa7bb923b40868c875a88f42f2a6691df773e02655e02d67bc75 src/leansearchv2/reasoning/filter.py
eae7d620d793ab6785a8a26eeee9ea943ae2dbe5124f14e5e1d3298ff8016a67 src/leansearchv2/reasoning/judge.py
1866d4261cb31eb01624b65b423d0768d3b1d1ac17fc31f7b5c3d77d9ef11682 src/leansearchv2/reasoning/prompts.py
d02c48677e00b9b81297311118c8d830994a6b6909ec330a9570cded57c34497 src/leansearchv2/reasoning/run.py
8f3a9232dd2109264b3f62169a3da92a3214d769112f41b679d046173b969985 src/leansearchv2/runtime.py
be4b8f8fa0cec78512e99024f1f1d1edb48f76b2c422c053985cd690a754d110 src/leansearchv2/server.py
e8b9dea2004116f863b24accb1f82f4d12c3f0e9d09e611cc18254662e9022fd src/leansearchv2/standard_client.py
5bc85a23d2ae257e52284dfc14ad197d4880576d1ab88fc5060ae89d4cf9d8df tests/__init__.py
57a7bc32d960b27cc0c554faa4f73d23d7804ce51d8d8e0c350e740bd440cca2 tests/test_gemini_vertex_web_search.py
fb2e9271bbf54f05a7a1adbd88b06104560117cf42b666a5dfcd43da9f175095 tests/test_graph_build_cli.py
24bd5819d6096e5cdd754fd4af06e706d6a049f427c07238f007e60a4931cfc1 tests/test_graph_core.py
dee484835a8f7c1d3919edf13b305476214aaceb62ee1ee3d82940721c7c07fb tests/test_llm_usage.py
2ae968a7e7c6ed96de172d663e876ac09c599ca2e462860bfef91d76189e934c tests/test_paper_entrypoints.py
f63b06e5c3ad8250fa488de9793796e9cd4d534ba326d7efbb5c214c105e5b78 tests/test_pipeline_graph_contract.py
a68610fde7345a4638c8d6290803134ad23f852bb880eb59d029da9421a6bdf0 tests/test_pipeline_graph_off_behavior.py
5db53e685e827f60acf240052965dad10a5dd325659c04652e0ec3d2a950a038 tests/test_pipeline_missing_graph.py
d2a777b2f916b7933c1778ea3cfdf8d463dbd7a3d4fd8111a437f7c23afdfe4c tests/test_premise_costed.py
dfbcd58ff557d540ce4b1c7f718f2a91702d3bb576e789f2757f64cebd7cce8a tests/test_prove_a2_budget.py
e3f6b59a1a709a441f534fe25da888f6bc77563003b6b14127b1a40c5658eecd tests/test_prove_body_transport.py
f2e38aff53ee0630fc90db71a3bc6552a8ddffe39d6865454d288d8e0507a27e tests/test_prove_failure_memory.py
e9db23f506ad70361e02a4fa25df066bff26e3417a63e177bbe70c4b9eb1a353 tests/test_prove_integrity.py
f19ae2941564908886168c517f49813ceece4bc579f2a4c02bfec1a415a8664f tests/test_prove_usage_telemetry.py
5da2e593fe876ed9c948ef9ccd863ea18fe80d6da93d229d2e8ddcc19c13295e tests/test_proving.py
78af18a4943d8dd6793a9bbad97e5972d543f344678d0880a2757e306bb55823 tests/test_reasoning_budget.py
c494b3a5fb4d58f3000b7fc1c9ca05382f4f21150d2b41640724372bed296c03 tests/test_reasoning_filter.py
407b22be32921e7c226fa1f4b426667bd89e8abcef0aead05c2a004f51e8c5d5 tests/test_search_metrics.py
123f44522ceac337b7103fb72a0d896e0d6d03d39dc59bbd501c78507bec175e tests/test_standard_client_graph.py
17d44c3960ef89b931ad4b99f935f6885afc0245193bb2d17f908a635229a0d1 tests/test_standard_graph_integration.py