[{"name":".gitignore","path":".gitignore","sha":"d03174196e0b259418afc6175bd1d072b12646cc","size":17,"url":"https://api.github.com/repos/openai/ten-proofs/contents/.gitignore?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/.gitignore","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/d03174196e0b259418afc6175bd1d072b12646cc","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/.gitignore","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/.gitignore?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/d03174196e0b259418afc6175bd1d072b12646cc","html":"https://github.com/openai/ten-proofs/blob/main/.gitignore"}},{"name":"All.lean","path":"All.lean","sha":"88c84b365294a8dfae3a48701ec6da73620bcdfa","size":242,"url":"https://api.github.com/repos/openai/ten-proofs/contents/All.lean?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/All.lean","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/88c84b365294a8dfae3a48701ec6da73620bcdfa","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/All.lean","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/All.lean?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/88c84b365294a8dfae3a48701ec6da73620bcdfa","html":"https://github.com/openai/ten-proofs/blob/main/All.lean"}},{"name":"CompactnessAndDegeneracy.lean","path":"CompactnessAndDegeneracy.lean","sha":"0e973d50014e8c800af597ef699ef29b81e42fc6","size":721769,"url":"https://api.github.com/repos/openai/ten-proofs/contents/CompactnessAndDegeneracy.lean?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/CompactnessAndDegeneracy.lean","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/0e973d50014e8c800af597ef699ef29b81e42fc6","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/CompactnessAndDegeneracy.lean","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/CompactnessAndDegeneracy.lean?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/0e973d50014e8c800af597ef699ef29b81e42fc6","html":"https://github.com/openai/ten-proofs/blob/main/CompactnessAndDegeneracy.lean"}},{"name":"ComparatorChallenges","path":"ComparatorChallenges","sha":"84e2aa4c3e60fd0927ba6a9a9e6f41a0ed18c954","size":0,"url":"https://api.github.com/repos/openai/ten-proofs/contents/ComparatorChallenges?ref=main","html_url":"https://github.com/openai/ten-proofs/tree/main/ComparatorChallenges","git_url":"https://api.github.com/repos/openai/ten-proofs/git/trees/84e2aa4c3e60fd0927ba6a9a9e6f41a0ed18c954","download_url":null,"type":"dir","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/ComparatorChallenges?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/trees/84e2aa4c3e60fd0927ba6a9a9e6f41a0ed18c954","html":"https://github.com/openai/ten-proofs/tree/main/ComparatorChallenges"}},{"name":"ConnesRigidity.lean","path":"ConnesRigidity.lean","sha":"81cf03e3f7ccdc66815cc00c9969bcfd2341c8d6","size":1449151,"url":"https://api.github.com/repos/openai/ten-proofs/contents/ConnesRigidity.lean?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/ConnesRigidity.lean","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/81cf03e3f7ccdc66815cc00c9969bcfd2341c8d6","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/ConnesRigidity.lean","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/ConnesRigidity.lean?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/81cf03e3f7ccdc66815cc00c9969bcfd2341c8d6","html":"https://github.com/openai/ten-proofs/blob/main/ConnesRigidity.lean"}},{"name":"EhrhartVolumeInequality.lean","path":"EhrhartVolumeInequality.lean","sha":"842c602ab882dfae64352fed0bce2d83c19b31e8","size":2163484,"url":"https://api.github.com/repos/openai/ten-proofs/contents/EhrhartVolumeInequality.lean?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/EhrhartVolumeInequality.lean","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/842c602ab882dfae64352fed0bce2d83c19b31e8","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/EhrhartVolumeInequality.lean","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/EhrhartVolumeInequality.lean?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/842c602ab882dfae64352fed0bce2d83c19b31e8","html":"https://github.com/openai/ten-proofs/blob/main/EhrhartVolumeInequality.lean"}},{"name":"GapCVP.lean","path":"GapCVP.lean","sha":"47f3a395e4d9ec3e2892664860f26ed63421b0c9","size":5335203,"url":"https://api.github.com/repos/openai/ten-proofs/contents/GapCVP.lean?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/GapCVP.lean","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/47f3a395e4d9ec3e2892664860f26ed63421b0c9","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/GapCVP.lean","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/GapCVP.lean?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/47f3a395e4d9ec3e2892664860f26ed63421b0c9","html":"https://github.com/openai/ten-proofs/blob/main/GapCVP.lean"}},{"name":"LICENSE","path":"LICENSE","sha":"261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64","size":11357,"url":"https://api.github.com/repos/openai/ten-proofs/contents/LICENSE?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/LICENSE","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/LICENSE","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/LICENSE?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64","html":"https://github.com/openai/ten-proofs/blob/main/LICENSE"}},{"name":"MetricCodes.lean","path":"MetricCodes.lean","sha":"51628c0db81bd6cb9a79777fa601306c9d64cbc5","size":4531268,"url":"https://api.github.com/repos/openai/ten-proofs/contents/MetricCodes.lean?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/MetricCodes.lean","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/51628c0db81bd6cb9a79777fa601306c9d64cbc5","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/MetricCodes.lean","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/MetricCodes.lean?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/51628c0db81bd6cb9a79777fa601306c9d64cbc5","html":"https://github.com/openai/ten-proofs/blob/main/MetricCodes.lean"}},{"name":"MulticolorTriangleRamsey.lean","path":"MulticolorTriangleRamsey.lean","sha":"24b55f531a4d36347cd2277b1b9c7d784d91ae35","size":125769,"url":"https://api.github.com/repos/openai/ten-proofs/contents/MulticolorTriangleRamsey.lean?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/MulticolorTriangleRamsey.lean","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/24b55f531a4d36347cd2277b1b9c7d784d91ae35","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/MulticolorTriangleRamsey.lean","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/MulticolorTriangleRamsey.lean?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/24b55f531a4d36347cd2277b1b9c7d784d91ae35","html":"https://github.com/openai/ten-proofs/blob/main/MulticolorTriangleRamsey.lean"}},{"name":"NonSoficGroup.lean","path":"NonSoficGroup.lean","sha":"dd1f8e63960300c8674fcd491007d2a628fbc6fe","size":1343031,"url":"https://api.github.com/repos/openai/ten-proofs/contents/NonSoficGroup.lean?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/NonSoficGroup.lean","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/dd1f8e63960300c8674fcd491007d2a628fbc6fe","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/NonSoficGroup.lean","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/NonSoficGroup.lean?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/dd1f8e63960300c8674fcd491007d2a628fbc6fe","html":"https://github.com/openai/ten-proofs/blob/main/NonSoficGroup.lean"}},{"name":"Permanent.lean","path":"Permanent.lean","sha":"56100e1ae26e6920a569166d0f4cdb4b42b04301","size":1131535,"url":"https://api.github.com/repos/openai/ten-proofs/contents/Permanent.lean?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/Permanent.lean","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/56100e1ae26e6920a569166d0f4cdb4b42b04301","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/Permanent.lean","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/Permanent.lean?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/56100e1ae26e6920a569166d0f4cdb4b42b04301","html":"https://github.com/openai/ten-proofs/blob/main/Permanent.lean"}},{"name":"QuantumParallelRepetition.lean","path":"QuantumParallelRepetition.lean","sha":"887c4378f124a5d81a3f2624b6dc34867ec409c4","size":2683872,"url":"https://api.github.com/repos/openai/ten-proofs/contents/QuantumParallelRepetition.lean?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/QuantumParallelRepetition.lean","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/887c4378f124a5d81a3f2624b6dc34867ec409c4","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/QuantumParallelRepetition.lean","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/QuantumParallelRepetition.lean?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/887c4378f124a5d81a3f2624b6dc34867ec409c4","html":"https://github.com/openai/ten-proofs/blob/main/QuantumParallelRepetition.lean"}},{"name":"README.md","path":"README.md","sha":"3b8381257d1ee2edd7912323cb4ceaa719572257","size":3042,"url":"https://api.github.com/repos/openai/ten-proofs/contents/README.md?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/README.md","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/3b8381257d1ee2edd7912323cb4ceaa719572257","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/README.md","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/README.md?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/3b8381257d1ee2edd7912323cb4ceaa719572257","html":"https://github.com/openai/ten-proofs/blob/main/README.md"}},{"name":"SpherePacking.lean","path":"SpherePacking.lean","sha":"e6117934a80142a8249356fdafa797eba030e920","size":2096663,"url":"https://api.github.com/repos/openai/ten-proofs/contents/SpherePacking.lean?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/SpherePacking.lean","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/e6117934a80142a8249356fdafa797eba030e920","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/SpherePacking.lean","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/SpherePacking.lean?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/e6117934a80142a8249356fdafa797eba030e920","html":"https://github.com/openai/ten-proofs/blob/main/SpherePacking.lean"}},{"name":"formalization.yaml","path":"formalization.yaml","sha":"63d31d019f0bcff6052191d3aac71d4191f34131","size":5399,"url":"https://api.github.com/repos/openai/ten-proofs/contents/formalization.yaml?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/formalization.yaml","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/63d31d019f0bcff6052191d3aac71d4191f34131","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/formalization.yaml","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/formalization.yaml?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/63d31d019f0bcff6052191d3aac71d4191f34131","html":"https://github.com/openai/ten-proofs/blob/main/formalization.yaml"}},{"name":"lake-manifest.json","path":"lake-manifest.json","sha":"046e8de7f46832fbf092e3fb815efae01e4a2129","size":4141,"url":"https://api.github.com/repos/openai/ten-proofs/contents/lake-manifest.json?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/lake-manifest.json","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/046e8de7f46832fbf092e3fb815efae01e4a2129","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/lake-manifest.json","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/lake-manifest.json?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/046e8de7f46832fbf092e3fb815efae01e4a2129","html":"https://github.com/openai/ten-proofs/blob/main/lake-manifest.json"}},{"name":"lakefile.toml","path":"lakefile.toml","sha":"f29d6b0307597932154b34b97e37fe07ec3356de","size":1548,"url":"https://api.github.com/repos/openai/ten-proofs/contents/lakefile.toml?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/lakefile.toml","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/f29d6b0307597932154b34b97e37fe07ec3356de","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/lakefile.toml","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/lakefile.toml?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/f29d6b0307597932154b34b97e37fe07ec3356de","html":"https://github.com/openai/ten-proofs/blob/main/lakefile.toml"}},{"name":"lean-toolchain","path":"lean-toolchain","sha":"94b9f495baff80fd9cb44aad8f4762cb3b2066fe","size":25,"url":"https://api.github.com/repos/openai/ten-proofs/contents/lean-toolchain?ref=main","html_url":"https://github.com/openai/ten-proofs/blob/main/lean-toolchain","git_url":"https://api.github.com/repos/openai/ten-proofs/git/blobs/94b9f495baff80fd9cb44aad8f4762cb3b2066fe","download_url":"https://raw.githubusercontent.com/openai/ten-proofs/main/lean-toolchain","type":"file","_links":{"self":"https://api.github.com/repos/openai/ten-proofs/contents/lean-toolchain?ref=main","git":"https://api.github.com/repos/openai/ten-proofs/git/blobs/94b9f495baff80fd9cb44aad8f4762cb3b2066fe","html":"https://github.com/openai/ten-proofs/blob/main/lean-toolchain"}}]