docs: fix broken relative links

README.md

@@ -152,7 +152,7 @@ benchmark files.
 ### 1. Pick a problem
 
 Generated workspaces live under `generated/`, one directory per problem. The current
-catalog is summarized in [`generated/index.json`](/home/kim/lean-evals/generated/index.json).
+catalog is summarized in [`generated/index.json`](generated/index.json).
 
 Examples:
 
@@ -347,13 +347,13 @@ In practice, solvers should normally work in `Submission.lean` and `Submission/`
 
 ## Repository Layout
 
-- [`LeanEval/`](/home/kim/lean-evals/LeanEval): trusted authored problem statements
+- [`LeanEval/`](LeanEval): trusted authored problem statements
 - [`manifests/problems/`](manifests/problems/): one TOML file per problem, named `<id>.toml`
 - [`manifests/tags.toml`](manifests/tags.toml): stable tag registry
 - [`manifests/sets/`](manifests/sets/): versioned and optionally frozen named problem sets
-- [`generated/`](/home/kim/lean-evals/generated): generated comparator workspaces
-- [`scripts/`](/home/kim/lean-evals/scripts): generation, validation, and scoring helpers
-- [`PLAN.md`](/home/kim/lean-evals/PLAN.md): deferred design and roadmap notes
+- [`generated/`](generated): generated comparator workspaces
+- [`scripts/`](scripts): generation, validation, and scoring helpers
+- [`PLAN.md`](PLAN.md): deferred design and roadmap notes
 
 ## End-To-End Repo Checks
 

SECURITY.md

@@ -68,10 +68,10 @@ verifier. Given a `config.json` listing `theorem_names`,
    every transitively-used constant (other than def-hole targets, where
    only the type signature must match) is byte-identical between
    Challenge and Solution. See
-   [comparator/Comparator/Compare.lean](../comparator/Comparator/Compare.lean).
+   [comparator/Comparator/Compare.lean](https://github.com/leanprover/comparator/blob/master/Comparator/Compare.lean).
 3. Walks the same graph for axioms and requires every reachable axiom
    to be in the `permitted_axioms` allowlist. See
-   [comparator/Comparator/Axioms.lean](../comparator/Comparator/Axioms.lean).
+   [comparator/Comparator/Axioms.lean](https://github.com/leanprover/comparator/blob/master/Comparator/Axioms.lean).
    Our allowlist is `{propext, Quot.sound, Classical.choice}`. Notably
    absent: `sorryAx` (so `sorry` is rejected) and `Lean.ofReduceBool`
    (so `native_decide` is rejected).
@@ -357,7 +357,7 @@ escaping, the triage gate) are in the submissions repo's `SECURITY.md`.
 
 ## References
 
-- [comparator/Main.lean](../comparator/Main.lean), [comparator/Comparator/Compare.lean](../comparator/Comparator/Compare.lean), [comparator/Comparator/Axioms.lean](../comparator/Comparator/Axioms.lean) — verifier internals.
+- [comparator/Main.lean](https://github.com/leanprover/comparator/blob/master/Main.lean), [comparator/Comparator/Compare.lean](https://github.com/leanprover/comparator/blob/master/Comparator/Compare.lean), [comparator/Comparator/Axioms.lean](https://github.com/leanprover/comparator/blob/master/Comparator/Axioms.lean) — verifier internals.
 - [leanprover/comparator README](https://github.com/leanprover/comparator) — upstream trust model.
 - [scripts/security_probes/](scripts/security_probes/) — the security probes cited above.
 - [scripts/action_pin_audit.py](scripts/action_pin_audit.py),

generated/radon_transform_inversion/README.md

@@ -11,7 +11,7 @@ Radon transform: Fourier-slice diagonalization and pseudo-inversion
 - Submitter: Kim Morrison
 - Notes: The Fourier slice theorem diagonalizes the Radon transform (1D Fourier of a projection = a 2D-Fourier slice), and the transform has a left inverse on Schwartz functions. Trusted helpers radon, fourier1, fourier2 (non-holes). Mathlib has the 1D/2D Fourier transforms and Schwartz space but no Radon transform, Fourier slice theorem, or filtered back-projection. The pseudo-inverse is stated existentially (the explicit filtered-back-projection form would need the Hilbert transform / Riesz potential). Candidate from §100 of the Knill survey.
 - Source: J. Radon (1917); R. N. Bracewell (Fourier slice theorem, 1956). Knill, *Some fundamental theorems in mathematics*, §100.
-- Informal solution: Fourier slice theorem: writing the Radon projection R f(p,θ) and taking its 1D Fourier transform in p, interchange integrals (Fubini) and change variables so the line-integral-then-Fourier becomes the 2D Fourier transform of f restricted to the line through the origin at angle θ: F₁[Rf(·,θ)](k) = F₂[f](k cos θ, k sin θ). This diagonalizes R (it becomes a slice/multiplication operator). Pseudo-inversion: the slice identity plus 2D Fourier inversion on Schwartz functions makes R injective on 𝓢, so a left inverse exists; the canonical one is filtered back-projection u ↦ backproject(Hilbert-filter(u)). Mathlib lacks the slice theorem and the filter.
+- Informal solution: Fourier slice theorem: writing the Radon projection R f(p,θ) and taking its 1D Fourier transform in p, interchange integrals (Fubini) and change variables so the line-integral-then-Fourier becomes the 2D Fourier transform of f restricted to the line through the origin at angle θ: F₁\[Rf(·,θ)\](k) = F₂[f](k cos θ, k sin θ). This diagonalizes R (it becomes a slice/multiplication operator). Pseudo-inversion: the slice identity plus 2D Fourier inversion on Schwartz functions makes R injective on 𝓢, so a left inverse exists; the canonical one is filtered back-projection u ↦ backproject(Hilbert-filter(u)). Mathlib lacks the slice theorem and the filter.
 
 Do not modify `Challenge.lean` or `Solution.lean`. Those files are part of the
 trusted benchmark and fixed by the repository.

manifests/problems/radon_transform_inversion.toml

@@ -10,7 +10,7 @@ holes = ["radon_can_be_diagonalized_and_pseudo_inverted"]
 submitter = "Kim Morrison"
 notes = "The Fourier slice theorem diagonalizes the Radon transform (1D Fourier of a projection = a 2D-Fourier slice), and the transform has a left inverse on Schwartz functions. Trusted helpers radon, fourier1, fourier2 (non-holes). Mathlib has the 1D/2D Fourier transforms and Schwartz space but no Radon transform, Fourier slice theorem, or filtered back-projection. The pseudo-inverse is stated existentially (the explicit filtered-back-projection form would need the Hilbert transform / Riesz potential). Candidate from §100 of the Knill survey."
 source = "J. Radon (1917); R. N. Bracewell (Fourier slice theorem, 1956). Knill, *Some fundamental theorems in mathematics*, §100."
-informal_solution = "Fourier slice theorem: writing the Radon projection R f(p,θ) and taking its 1D Fourier transform in p, interchange integrals (Fubini) and change variables so the line-integral-then-Fourier becomes the 2D Fourier transform of f restricted to the line through the origin at angle θ: F₁[Rf(·,θ)](k) = F₂[f](k cos θ, k sin θ). This diagonalizes R (it becomes a slice/multiplication operator). Pseudo-inversion: the slice identity plus 2D Fourier inversion on Schwartz functions makes R injective on 𝓢, so a left inverse exists; the canonical one is filtered back-projection u ↦ backproject(Hilbert-filter(u)). Mathlib lacks the slice theorem and the filter."
+informal_solution = "Fourier slice theorem: writing the Radon projection R f(p,θ) and taking its 1D Fourier transform in p, interchange integrals (Fubini) and change variables so the line-integral-then-Fourier becomes the 2D Fourier transform of f restricted to the line through the origin at angle θ: F₁\\[Rf(·,θ)\\](k) = F₂[f](k cos θ, k sin θ). This diagonalizes R (it becomes a slice/multiplication operator). Pseudo-inversion: the slice identity plus 2D Fourier inversion on Schwartz functions makes R injective on 𝓢, so a left inverse exists; the canonical one is filtered back-projection u ↦ backproject(Hilbert-filter(u)). Mathlib lacks the slice theorem and the filter."
 
 [[status_history]]
 status = "archived"