-
Notifications
You must be signed in to change notification settings - Fork 9
benchmarks: add Littlewood certified finite search #598
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit
Hold shift + click to select a range
277d582
benchmarks: add Littlewood certified finite search
477ffa5
fix(benchmarks): remove Littlewood evidence cap and decouple mathematics
morluto 543fc5e
fix(benchmarks): repair littlewood-certified-finite-search CI contrac…
cursoragent 6fa75d5
fix(benchmarks): preserve diagnostics for schema-invalid assurance an…
morluto File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
12 changes: 12 additions & 0 deletions
12
...arks/datasets/conjecture-probes-v1/littlewood-certified-finite-search/README.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,12 @@ | ||
| # Littlewood certified finite search | ||
|
|
||
| Assurance task from retained row C-015. Its sole objective is rigorous finite | ||
| Diophantine-approximation search: reconstruct all record minima using exact | ||
| rational square-root enclosures, not floating point. The full 2000-point range | ||
| is independently replayed and the global finite winner must be interval- | ||
| separated from every competitor. | ||
|
|
||
| Difficulty is provisional Hard because nearest-integer branches, 80-digit | ||
| rational bounds, complete record logic, and scope calibration must agree. | ||
| Source: <https://mathworld.wolfram.com/LittlewoodConjecture.html>, status | ||
| checked 2026-08-06. No finite outcome is treated as a liminf result. |
3 changes: 3 additions & 0 deletions
3
...s/datasets/conjecture-probes-v1/littlewood-certified-finite-search/environment/Dockerfile
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,3 @@ | ||
| FROM python:3.12-slim@sha256:57cd7c3a7a273101a6485ba99423ee568157882804b1124b4dd04266317710de | ||
| COPY input.json submission_schema.json /app/ | ||
| WORKDIR /app |
1 change: 1 addition & 0 deletions
1
...s/datasets/conjecture-probes-v1/littlewood-certified-finite-search/environment/input.json
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| {"task_id":"jacobian/littlewood-certified-finite-search","conjecture_id":"C-015","radicands":[2,3],"n_min":1,"n_max":2000,"sqrt_scale_digits":80,"scope":"sqrt2-sqrt3-n-up-to-2000-v1"} |
150 changes: 150 additions & 0 deletions
150
...onjecture-probes-v1/littlewood-certified-finite-search/environment/submission_schema.json
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,150 @@ | ||
| { | ||
| "$defs": { | ||
| "rat": { | ||
| "pattern": "^[0-9]+(?:/[1-9][0-9]*)?$", | ||
| "type": "string" | ||
| }, | ||
| "record": { | ||
| "additionalProperties": false, | ||
| "properties": { | ||
| "floors": { | ||
| "items": { | ||
| "minimum": 1, | ||
| "type": "integer" | ||
| }, | ||
| "maxItems": 2, | ||
| "minItems": 2, | ||
| "type": "array" | ||
| }, | ||
| "lower": { | ||
| "$ref": "#/$defs/rat" | ||
| }, | ||
| "n": { | ||
| "maximum": 2000, | ||
| "minimum": 1, | ||
| "type": "integer" | ||
| }, | ||
| "nearest": { | ||
| "items": { | ||
| "minimum": 1, | ||
| "type": "integer" | ||
| }, | ||
| "maxItems": 2, | ||
| "minItems": 2, | ||
| "type": "array" | ||
| }, | ||
| "upper": { | ||
| "$ref": "#/$defs/rat" | ||
| } | ||
| }, | ||
| "required": [ | ||
| "n", | ||
| "floors", | ||
| "nearest", | ||
| "lower", | ||
| "upper" | ||
| ], | ||
| "type": "object" | ||
| } | ||
| }, | ||
| "$schema": "https://json-schema.org/draft/2020-12/schema", | ||
| "additionalProperties": false, | ||
| "properties": { | ||
| "claimed_assurance": { | ||
| "enum": [ | ||
| "UNVERIFIED", | ||
| "COMPUTED", | ||
| "CHECKED", | ||
| "VERIFIED" | ||
| ] | ||
| }, | ||
| "completeness": { | ||
| "const": "COMPLETE" | ||
| }, | ||
| "conclusion": { | ||
| "const": "LITTLEWOOD_FINITE_MINIMUM_CERTIFICATE" | ||
| }, | ||
| "evidence": { | ||
| "items": { | ||
| "additionalProperties": false, | ||
| "properties": { | ||
| "path": { | ||
| "const": "evidence/answer.txt" | ||
| }, | ||
| "sha256": { | ||
| "pattern": "^sha256:[0-9a-f]{64}$", | ||
| "type": "string" | ||
| } | ||
| }, | ||
| "required": [ | ||
| "path", | ||
| "sha256" | ||
| ], | ||
| "type": "object" | ||
| }, | ||
| "maxItems": 1, | ||
| "minItems": 1, | ||
| "type": "array" | ||
| }, | ||
| "limitations": { | ||
| "const": [ | ||
| "ONE_FIXED_QUADRATIC_IRRATIONAL_PAIR", | ||
| "N_AT_MOST_2000", | ||
| "NO_LIMINF_OR_LITTLEWOOD_CONCLUSION" | ||
| ] | ||
| }, | ||
| "result": { | ||
| "additionalProperties": false, | ||
| "properties": { | ||
| "argmin_n": { | ||
| "maximum": 2000, | ||
| "minimum": 1, | ||
| "type": "integer" | ||
| }, | ||
| "comparison_status": { | ||
| "const": "STRICTLY_SEPARATED_INTERVALS" | ||
| }, | ||
| "minimum_lower": { | ||
| "$ref": "#/$defs/rat" | ||
| }, | ||
| "minimum_upper": { | ||
| "$ref": "#/$defs/rat" | ||
| }, | ||
| "records": { | ||
| "items": { | ||
| "$ref": "#/$defs/record" | ||
| }, | ||
| "maxItems": 100, | ||
| "minItems": 2, | ||
| "type": "array" | ||
| } | ||
| }, | ||
| "required": [ | ||
| "records", | ||
| "argmin_n", | ||
| "minimum_lower", | ||
| "minimum_upper", | ||
| "comparison_status" | ||
| ], | ||
| "type": "object" | ||
| }, | ||
| "scope": { | ||
| "const": "sqrt2-sqrt3-n-up-to-2000-v1", | ||
| "type": "string" | ||
| }, | ||
| "task_id": { | ||
| "const": "jacobian/littlewood-certified-finite-search" | ||
| } | ||
| }, | ||
| "required": [ | ||
| "task_id", | ||
| "conclusion", | ||
| "result", | ||
| "claimed_assurance", | ||
| "scope", | ||
| "completeness", | ||
| "evidence", | ||
| "limitations" | ||
| ], | ||
| "type": "object" | ||
| } |
33 changes: 33 additions & 0 deletions
33
...datasets/conjecture-probes-v1/littlewood-certified-finite-search/instruction.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,33 @@ | ||
| # Certify a finite Littlewood-product minimum | ||
|
|
||
| For every integer `1 <= n <= 2000`, consider | ||
| `n ||n sqrt(2)|| ||n sqrt(3)||`. Use rigorous rational lower and upper | ||
| enclosures obtained from the frozen 80-digit integer-square-root scale, never | ||
| floating point. Submit the complete strict record-minimum sequence. Each row | ||
| must include `n`, the two floor values, the two nearest integers, and canonical | ||
| rational lower/upper bounds for the product. Identify the final finite argmin. | ||
|
|
||
| The verifier independently reconstructs all 2000 enclosures and the complete | ||
| record sequence. Evidence is a matching JSON object (`application/json`) with | ||
| exactly `schema_version` (the string `"1"`), `task_id`, `result`, and | ||
| `limitations`. | ||
|
|
||
| This certifies only the frozen finite range for `(sqrt(2),sqrt(3))`; it does not | ||
| establish a liminf or any case of Littlewood's conjecture. | ||
|
|
||
| <!-- BEGIN PUBLIC CONTRACT SUBMISSION BLOCK --> | ||
| ## Submission | ||
|
|
||
| Rigorous rational interval replay for a finite range only; no Littlewood conclusion. | ||
|
|
||
| Write `/app/submission.json` to the exact schema in `environment/submission_schema.json`. The submission envelope requires `task_id`, `conclusion`, `result`, `claimed_assurance`, `scope`, `completeness`, `evidence`, and `limitations`. | ||
|
|
||
| - **Conclusion:** exactly `LITTLEWOOD_FINITE_MINIMUM_CERTIFICATE` | ||
| - **Assurance:** scoreable values are `UNVERIFIED`, `COMPUTED`, `CHECKED` (ceiling `CHECKED`); the submission schema accepts any of `UNVERIFIED`, `COMPUTED`, `CHECKED`, `VERIFIED` but only scoreable assurances receive credit. | ||
| - **Scope:** the exact value declared in `submission_schema.json` | ||
| - **Completeness:** `COMPLETE`. | ||
| - **Evidence:** 1-1 item(s); allowed path(s): `evidence/answer.txt`; digest must match `^sha256:[0-9a-f]{64}$`. | ||
| - **Evidence media types:** `application/json`. | ||
| - **Evidence payload:** JSON object with exactly `schema_version` (string `"1"`), `task_id`, `result`, and `limitations`. | ||
| - **Required artifact filenames:** `evidence/answer.txt`. | ||
| <!-- END PUBLIC CONTRACT SUBMISSION BLOCK --> |
87 changes: 87 additions & 0 deletions
87
...hmarks/datasets/conjecture-probes-v1/littlewood-certified-finite-search/solution/solve.py
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,87 @@ | ||
| from __future__ import annotations | ||
|
|
||
| import argparse | ||
| import hashlib | ||
| import json | ||
| from fractions import Fraction | ||
| from math import isqrt | ||
| from pathlib import Path | ||
|
|
||
| TASK_ID = "jacobian/littlewood-certified-finite-search" | ||
| LIMITATIONS = [ | ||
| "ONE_FIXED_QUADRATIC_IRRATIONAL_PAIR", | ||
| "N_AT_MOST_2000", | ||
| "NO_LIMINF_OR_LITTLEWOOD_CONCLUSION", | ||
| ] | ||
| SCALE = 10**80 | ||
|
|
||
|
|
||
| def bounds(d, n): | ||
| root = isqrt(d * SCALE * SCALE) | ||
| lo = Fraction(root, SCALE) | ||
| hi = Fraction(root + 1, SCALE) | ||
| floor = isqrt(d * n * n) | ||
| if 4 * d * n * n < (2 * floor + 1) ** 2: | ||
| return floor, floor, n * lo - floor, n * hi - floor | ||
| return floor, floor + 1, floor + 1 - n * hi, floor + 1 - n * lo | ||
|
|
||
|
|
||
| def row(n): | ||
| a = bounds(2, n) | ||
| b = bounds(3, n) | ||
| return { | ||
| "n": n, | ||
| "floors": [a[0], b[0]], | ||
| "nearest": [a[1], b[1]], | ||
| "lower": str(n * a[2] * b[2]), | ||
| "upper": str(n * a[3] * b[3]), | ||
| } | ||
|
|
||
|
|
||
| def main(): | ||
| parser = argparse.ArgumentParser() | ||
| parser.add_argument("--root", type=Path, default=Path("/app")) | ||
| root = parser.parse_args().root | ||
| records = [] | ||
| best = None | ||
| for n in range(1, 2001): | ||
| current = row(n) | ||
| if best is None or Fraction(current["upper"]) < Fraction(best["lower"]): | ||
| records.append(current) | ||
| best = current | ||
| result = { | ||
| "records": records, | ||
| "argmin_n": best["n"], | ||
| "minimum_lower": best["lower"], | ||
| "minimum_upper": best["upper"], | ||
| "comparison_status": "STRICTLY_SEPARATED_INTERVALS", | ||
| } | ||
| payload = { | ||
| "schema_version": "1", | ||
| "task_id": TASK_ID, | ||
| "result": result, | ||
| "limitations": LIMITATIONS, | ||
| } | ||
| e = root / "evidence/answer.txt" | ||
| e.parent.mkdir(parents=True, exist_ok=True) | ||
| e.write_text(json.dumps(payload, sort_keys=True, separators=(",", ":")) + "\n") | ||
| s = { | ||
| "task_id": TASK_ID, | ||
| "conclusion": "LITTLEWOOD_FINITE_MINIMUM_CERTIFICATE", | ||
| "result": result, | ||
| "claimed_assurance": "CHECKED", | ||
| "scope": "sqrt2-sqrt3-n-up-to-2000-v1", | ||
| "completeness": "COMPLETE", | ||
| "evidence": [ | ||
| { | ||
| "path": "evidence/answer.txt", | ||
| "sha256": "sha256:" + hashlib.sha256(e.read_bytes()).hexdigest(), | ||
| } | ||
| ], | ||
| "limitations": LIMITATIONS, | ||
| } | ||
| (root / "submission.json").write_text(json.dumps(s, sort_keys=True) + "\n") | ||
|
|
||
|
|
||
| if __name__ == "__main__": | ||
| main() |
3 changes: 3 additions & 0 deletions
3
...hmarks/datasets/conjecture-probes-v1/littlewood-certified-finite-search/solution/solve.sh
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,3 @@ | ||
| #!/bin/sh | ||
| set -eu | ||
| python /solution/solve.py |
39 changes: 39 additions & 0 deletions
39
benchmarks/datasets/conjecture-probes-v1/littlewood-certified-finite-search/task.toml
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,39 @@ | ||
| schema_version="1.4" | ||
| artifacts=["/app/submission.json","/app/evidence"] | ||
| [task] | ||
| name="jacobian/littlewood-certified-finite-search" | ||
| version="1.0.0" | ||
| description="Certify a complete finite record-minimum search for n||n sqrt2||||n sqrt3|| using rigorous rational intervals." | ||
| keywords=["littlewood","diophantine-approximation","interval-certificates"] | ||
| [metadata] | ||
| evaluation_kind="conjecture-probe" | ||
| domain="mathematical-sciences" | ||
| primary_domain="number-theory" | ||
| field="diophantine-approximation" | ||
| assurance_ceiling="CHECKED" | ||
| answer_visibility="public" | ||
| provenance_class="authored-conjecture-probe" | ||
| fixture_digest="sha256:2cf9bff59f47bce08ec9e39dde6c8eb7700af3149a01e72003ce91fffedaaee9" | ||
| required_provider="core" | ||
| author_name="Jacobian contributors" | ||
| difficulty="hard" | ||
| category="mathematics" | ||
| tags=["difficulty-provisional","diophantine-approximation","rigorous-intervals","offline"] | ||
| case_version="conjecture-probes-v1" | ||
| contamination_class="authored-finite-conjecture-probe" | ||
| derivation="Derived from retained spreadsheet row C-015; the sqrt(2), sqrt(3), n<=2000 fixture is authored and finite." | ||
| [agent] | ||
| timeout_sec=600.0 | ||
| [verifier] | ||
| timeout_sec=120.0 | ||
| environment_mode="separate" | ||
| [environment] | ||
| network_mode="no-network" | ||
| cpus=1 | ||
| memory_mb=1024 | ||
| storage_mb=4096 | ||
| [verifier.environment] | ||
| network_mode="no-network" | ||
| cpus=1 | ||
| memory_mb=1024 | ||
| storage_mb=4096 |
7 changes: 7 additions & 0 deletions
7
benchmarks/datasets/conjecture-probes-v1/littlewood-certified-finite-search/tests/Dockerfile
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,7 @@ | ||
| FROM python:3.12-slim@sha256:57cd7c3a7a273101a6485ba99423ee568157882804b1124b4dd04266317710de | ||
| LABEL jacobian.task="jacobian/littlewood-certified-finite-search" \ | ||
| jacobian.checksum="592a711cf0c3a06c2eb0a86c967320e3928ac394a389bbdc7765f102b0290f62" | ||
| RUN python -m pip install --no-cache-dir attrs==26.1.0 jsonschema==4.26.0 jsonschema-specifications==2025.9.1 referencing==0.37.0 rpds-py==2026.6.3 typing-extensions==4.16.0 | ||
| COPY input.json public_contract.json test.sh verifier.py verifier_support.py /tests/ | ||
| COPY input.json /app/input.json | ||
| RUN chmod +x /tests/test.sh && python -c 'import json; assert json.load(open("/tests/input.json"))["task_id"] == "jacobian/littlewood-certified-finite-search"' | ||
1 change: 1 addition & 0 deletions
1
benchmarks/datasets/conjecture-probes-v1/littlewood-certified-finite-search/tests/input.json
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| {"task_id":"jacobian/littlewood-certified-finite-search","conjecture_id":"C-015","radicands":[2,3],"n_min":1,"n_max":2000,"sqrt_scale_digits":80,"scope":"sqrt2-sqrt3-n-up-to-2000-v1"} |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.