diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml
index 4312e8ec4..d97e9a2e6 100644
--- a/.github/workflows/bench-main.yml
+++ b/.github/workflows/bench-main.yml
@@ -128,8 +128,7 @@ jobs:
         # lake target (Compile<env>), the cache-key suffix, and the
         # bencher row name. Every registry env compiles here; which envs
         # the benchmark job then proves/checks depends on which envs have
-        # constants in Ix/BenchConstants.lean. Add FC once it's on
-        # current Lean.
+        # constants in Ix/BenchConstants.lean.
         include:
           - { env: InitStd }
           - { env: Lean }
@@ -139,7 +138,6 @@ jobs:
           - { env: ISLB }
           - { env: Mathlib, mathlib: true }
           - { env: FLT, cache_pkg: flt, mathlib: true }
-          # - { env: FC, cache_pkg: formal_conjectures, mathlib: true }
     steps:
       - uses: actions/checkout@v7
       # `lake build` below clones this package's Lake dependencies.
@@ -154,10 +152,6 @@ jobs:
           label: Compile measurement CPU
           provenance-file: ~/.local/bin/benchmark-build-cpu.txt
       - run: echo "$HOME/.local/bin" >> $GITHUB_PATH
-      # FC's library env lives in a sibling `${COMPILE_DIR}FC` package dir, so
-      # point COMPILE_DIR there for the FC matrix job.
-      # - if: matrix.env == 'FC'
-      #   run: echo "COMPILE_DIR=${{ env.COMPILE_DIR }}FC" | tee -a $GITHUB_ENV
       # Install the Lean toolchain. The mathlib olean cache is fetched only
       # for envs that import Mathlib (Mathlib, FLT) — the shared
       # Benchmarks/Compile package depends on mathlib, so without this
@@ -168,14 +162,12 @@ jobs:
           auto-config: false
           use-github-cache: false
           use-mathlib-cache: ${{ matrix.mathlib && 'true' || 'false' }}
-      # FLT and FC take a few minutes to rebuild, so cache their build artifacts.
+      # FLT takes a few minutes to rebuild, so cache its build artifacts.
       - if: matrix.cache_pkg
         uses: actions/cache@v6
         with:
           path: ${{ env.COMPILE_DIR }}/.lake/packages/${{ matrix.cache_pkg }}/.lake/build
           key: ${{ matrix.cache_pkg }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }}
-      # No `--wfail` here: formal-conjectures (FC) emits a copyright-notice
-      # warning that must not fail the build.
       - run: lake build Compile${{ matrix.env }}
         working-directory: ${{ env.COMPILE_DIR }}
       # The measured compile: serializes the env to `<env>.ixe` at the
diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml
index a5089f05f..f2d50dc64 100644
--- a/.github/workflows/update.yml
+++ b/.github/workflows/update.yml
@@ -35,8 +35,7 @@ jobs:
           # The root package plus every package under Benchmarks/ — `/**`
           # walks the whole tree (catching Catalog's nested fixture
           # workspaces) and skips dotted directories, so `.lake`
-          # dependency checkouts are never swept up. This includes
-          # Benchmarks/CompileFC, previously pinned to an old toolchain.
+          # dependency checkouts are never swept up.
           lake_package_directory: ". Benchmarks/**"
           bump_mode: pinned-tags
           pr: true
diff --git a/Benchmarks/CompileFC/.envrc b/Benchmarks/CompileFC/.envrc
deleted file mode 100644
index 3550a30f2..000000000
--- a/Benchmarks/CompileFC/.envrc
+++ /dev/null
@@ -1 +0,0 @@
-use flake
diff --git a/Benchmarks/CompileFC/CompileFC.lean b/Benchmarks/CompileFC/CompileFC.lean
deleted file mode 100644
index bf053aea1..000000000
--- a/Benchmarks/CompileFC/CompileFC.lean
+++ /dev/null
@@ -1,585 +0,0 @@
-import FormalConjectures.Arxiv.«0911.2077».Conjecture6_3
-import FormalConjectures.Arxiv.«0912.2382».CurlingNumberConjecture
-import FormalConjectures.Arxiv.«1308.0994».BoxdotConjecture
-import FormalConjectures.Arxiv.«1506.05785».MaximumAngle
-import FormalConjectures.Arxiv.«1601.03081».UniqueCrystalComponents
-import FormalConjectures.Arxiv.«1609.08688».sIncreasingrTuples
-import FormalConjectures.Arxiv.«2107.00295».IndependentDomination
-import FormalConjectures.Arxiv.«2107.12475».CollatzLike
-import FormalConjectures.Arxiv.«2208.14736».ZariskiCancellation
-import FormalConjectures.Arxiv.«2501.03234».ArithmeticSumS
-import FormalConjectures.Arxiv.«2504.17644».Margulis
-import FormalConjectures.Arxiv.«2602.05192».FirstProof4
-import FormalConjectures.Arxiv.«2602.05192».FirstProof6
-import FormalConjectures.Books.UniformDistributionOfSequences.Equidistribution
-import FormalConjectures.ErdosProblems.«1003»
-import FormalConjectures.ErdosProblems.«1004»
-import FormalConjectures.ErdosProblems.«100»
-import FormalConjectures.ErdosProblems.«1038»
-import FormalConjectures.ErdosProblems.«1041»
-import FormalConjectures.ErdosProblems.«1043»
-import FormalConjectures.ErdosProblems.«1049»
-import FormalConjectures.ErdosProblems.«1051»
-import FormalConjectures.ErdosProblems.«1052»
-import FormalConjectures.ErdosProblems.«1054»
-import FormalConjectures.ErdosProblems.«1055»
-import FormalConjectures.ErdosProblems.«1056»
-import FormalConjectures.ErdosProblems.«1059»
-import FormalConjectures.ErdosProblems.«1060»
-import FormalConjectures.ErdosProblems.«1061»
-import FormalConjectures.ErdosProblems.«1062»
-import FormalConjectures.ErdosProblems.«1063»
-import FormalConjectures.ErdosProblems.«1064»
-import FormalConjectures.ErdosProblems.«1065»
-import FormalConjectures.ErdosProblems.«1067»
-import FormalConjectures.ErdosProblems.«1068»
-import FormalConjectures.ErdosProblems.«1071»
-import FormalConjectures.ErdosProblems.«1072»
-import FormalConjectures.ErdosProblems.«1073»
-import FormalConjectures.ErdosProblems.«1074»
-import FormalConjectures.ErdosProblems.«1077»
-import FormalConjectures.ErdosProblems.«107»
-import FormalConjectures.ErdosProblems.«1080»
-import FormalConjectures.ErdosProblems.«1084»
-import FormalConjectures.ErdosProblems.«1085»
-import FormalConjectures.ErdosProblems.«108»
-import FormalConjectures.ErdosProblems.«1092»
-import FormalConjectures.ErdosProblems.«1093»
-import FormalConjectures.ErdosProblems.«1094»
-import FormalConjectures.ErdosProblems.«1095»
-import FormalConjectures.ErdosProblems.«1097»
-import FormalConjectures.ErdosProblems.«109»
-import FormalConjectures.ErdosProblems.«10»
-import FormalConjectures.ErdosProblems.«1101»
-import FormalConjectures.ErdosProblems.«1102»
-import FormalConjectures.ErdosProblems.«1104»
-import FormalConjectures.ErdosProblems.«1105»
-import FormalConjectures.ErdosProblems.«1106»
-import FormalConjectures.ErdosProblems.«1107»
-import FormalConjectures.ErdosProblems.«1108»
-import FormalConjectures.ErdosProblems.«1135»
-import FormalConjectures.ErdosProblems.«1137»
-import FormalConjectures.ErdosProblems.«1139»
-import FormalConjectures.ErdosProblems.«1141»
-import FormalConjectures.ErdosProblems.«1145»
-import FormalConjectures.ErdosProblems.«1148»
-import FormalConjectures.ErdosProblems.«1150»
-import FormalConjectures.ErdosProblems.«1176»
-import FormalConjectures.ErdosProblems.«119»
-import FormalConjectures.ErdosProblems.«11»
-import FormalConjectures.ErdosProblems.«120»
-import FormalConjectures.ErdosProblems.«123»
-import FormalConjectures.ErdosProblems.«124»
-import FormalConjectures.ErdosProblems.«125»
-import FormalConjectures.ErdosProblems.«126»
-import FormalConjectures.ErdosProblems.«128»
-import FormalConjectures.ErdosProblems.«12»
-import FormalConjectures.ErdosProblems.«137»
-import FormalConjectures.ErdosProblems.«138»
-import FormalConjectures.ErdosProblems.«139»
-import FormalConjectures.ErdosProblems.«13»
-import FormalConjectures.ErdosProblems.«141»
-import FormalConjectures.ErdosProblems.«142»
-import FormalConjectures.ErdosProblems.«143»
-import FormalConjectures.ErdosProblems.«145»
-import FormalConjectures.ErdosProblems.«14»
-import FormalConjectures.ErdosProblems.«152»
-import FormalConjectures.ErdosProblems.«153»
-import FormalConjectures.ErdosProblems.«155»
-import FormalConjectures.ErdosProblems.«158»
-import FormalConjectures.ErdosProblems.«160»
-import FormalConjectures.ErdosProblems.«168»
-import FormalConjectures.ErdosProblems.«170»
-import FormalConjectures.ErdosProblems.«172»
-import FormalConjectures.ErdosProblems.«17»
-import FormalConjectures.ErdosProblems.«188»
-import FormalConjectures.ErdosProblems.«189»
-import FormalConjectures.ErdosProblems.«194»
-import FormalConjectures.ErdosProblems.«195»
-import FormalConjectures.ErdosProblems.«196»
-import FormalConjectures.ErdosProblems.«197»
-import FormalConjectures.ErdosProblems.«198»
-import FormalConjectures.ErdosProblems.«1»
-import FormalConjectures.ErdosProblems.«200»
-import FormalConjectures.ErdosProblems.«203»
-import FormalConjectures.ErdosProblems.«204»
-import FormalConjectures.ErdosProblems.«208»
-import FormalConjectures.ErdosProblems.«20»
-import FormalConjectures.ErdosProblems.«212»
-import FormalConjectures.ErdosProblems.«213»
-import FormalConjectures.ErdosProblems.«218»
-import FormalConjectures.ErdosProblems.«219»
-import FormalConjectures.ErdosProblems.«228»
-import FormalConjectures.ErdosProblems.«229»
-import FormalConjectures.ErdosProblems.«233»
-import FormalConjectures.ErdosProblems.«234»
-import FormalConjectures.ErdosProblems.«236»
-import FormalConjectures.ErdosProblems.«238»
-import FormalConjectures.ErdosProblems.«239»
-import FormalConjectures.ErdosProblems.«23»
-import FormalConjectures.ErdosProblems.«242»
-import FormalConjectures.ErdosProblems.«243»
-import FormalConjectures.ErdosProblems.«244»
-import FormalConjectures.ErdosProblems.«245»
-import FormalConjectures.ErdosProblems.«247»
-import FormalConjectures.ErdosProblems.«248»
-import FormalConjectures.ErdosProblems.«249»
-import FormalConjectures.ErdosProblems.«250»
-import FormalConjectures.ErdosProblems.«251»
-import FormalConjectures.ErdosProblems.«252»
-import FormalConjectures.ErdosProblems.«253»
-import FormalConjectures.ErdosProblems.«257»
-import FormalConjectures.ErdosProblems.«258»
-import FormalConjectures.ErdosProblems.«259»
-import FormalConjectures.ErdosProblems.«25»
-import FormalConjectures.ErdosProblems.«263»
-import FormalConjectures.ErdosProblems.«264»
-import FormalConjectures.ErdosProblems.«266»
-import FormalConjectures.ErdosProblems.«267»
-import FormalConjectures.ErdosProblems.«268»
-import FormalConjectures.ErdosProblems.«269»
-import FormalConjectures.ErdosProblems.«26»
-import FormalConjectures.ErdosProblems.«273»
-import FormalConjectures.ErdosProblems.«274»
-import FormalConjectures.ErdosProblems.«275»
-import FormalConjectures.ErdosProblems.«276»
-import FormalConjectures.ErdosProblems.«277»
-import FormalConjectures.ErdosProblems.«283»
-import FormalConjectures.ErdosProblems.«285»
-import FormalConjectures.ErdosProblems.«288»
-import FormalConjectures.ErdosProblems.«289»
-import FormalConjectures.ErdosProblems.«28»
-import FormalConjectures.ErdosProblems.«295»
-import FormalConjectures.ErdosProblems.«298»
-import FormalConjectures.ErdosProblems.«299»
-import FormalConjectures.ErdosProblems.«303»
-import FormalConjectures.ErdosProblems.«304»
-import FormalConjectures.ErdosProblems.«306»
-import FormalConjectures.ErdosProblems.«307»
-import FormalConjectures.ErdosProblems.«30»
-import FormalConjectures.ErdosProblems.«312»
-import FormalConjectures.ErdosProblems.«313»
-import FormalConjectures.ErdosProblems.«316»
-import FormalConjectures.ErdosProblems.«317»
-import FormalConjectures.ErdosProblems.«318»
-import FormalConjectures.ErdosProblems.«319»
-import FormalConjectures.ErdosProblems.«321»
-import FormalConjectures.ErdosProblems.«324»
-import FormalConjectures.ErdosProblems.«325»
-import FormalConjectures.ErdosProblems.«326»
-import FormalConjectures.ErdosProblems.«329»
-import FormalConjectures.ErdosProblems.«32»
-import FormalConjectures.ErdosProblems.«330»
-import FormalConjectures.ErdosProblems.«331»
-import FormalConjectures.ErdosProblems.«332»
-import FormalConjectures.ErdosProblems.«33»
-import FormalConjectures.ErdosProblems.«340»
-import FormalConjectures.ErdosProblems.«341»
-import FormalConjectures.ErdosProblems.«346»
-import FormalConjectures.ErdosProblems.«347»
-import FormalConjectures.ErdosProblems.«348»
-import FormalConjectures.ErdosProblems.«349»
-import FormalConjectures.ErdosProblems.«350»
-import FormalConjectures.ErdosProblems.«351»
-import FormalConjectures.ErdosProblems.«352»
-import FormalConjectures.ErdosProblems.«354»
-import FormalConjectures.ErdosProblems.«355»
-import FormalConjectures.ErdosProblems.«357»
-import FormalConjectures.ErdosProblems.«358»
-import FormalConjectures.ErdosProblems.«359»
-import FormalConjectures.ErdosProblems.«361»
-import FormalConjectures.ErdosProblems.«364»
-import FormalConjectures.ErdosProblems.«366»
-import FormalConjectures.ErdosProblems.«36»
-import FormalConjectures.ErdosProblems.«370»
-import FormalConjectures.ErdosProblems.«371»
-import FormalConjectures.ErdosProblems.«373»
-import FormalConjectures.ErdosProblems.«375»
-import FormalConjectures.ErdosProblems.«376»
-import FormalConjectures.ErdosProblems.«377»
-import FormalConjectures.ErdosProblems.«379»
-import FormalConjectures.ErdosProblems.«383»
-import FormalConjectures.ErdosProblems.«385»
-import FormalConjectures.ErdosProblems.«386»
-import FormalConjectures.ErdosProblems.«387»
-import FormalConjectures.ErdosProblems.«389»
-import FormalConjectures.ErdosProblems.«38»
-import FormalConjectures.ErdosProblems.«390»
-import FormalConjectures.ErdosProblems.«392»
-import FormalConjectures.ErdosProblems.«394»
-import FormalConjectures.ErdosProblems.«396»
-import FormalConjectures.ErdosProblems.«397»
-import FormalConjectures.ErdosProblems.«398»
-import FormalConjectures.ErdosProblems.«399»
-import FormalConjectures.ErdosProblems.«39»
-import FormalConjectures.ErdosProblems.«3»
-import FormalConjectures.ErdosProblems.«402»
-import FormalConjectures.ErdosProblems.«406»
-import FormalConjectures.ErdosProblems.«409»
-import FormalConjectures.ErdosProblems.«40»
-import FormalConjectures.ErdosProblems.«410»
-import FormalConjectures.ErdosProblems.«412»
-import FormalConjectures.ErdosProblems.«413»
-import FormalConjectures.ErdosProblems.«414»
-import FormalConjectures.ErdosProblems.«416»
-import FormalConjectures.ErdosProblems.«417»
-import FormalConjectures.ErdosProblems.«418»
-import FormalConjectures.ErdosProblems.«41»
-import FormalConjectures.ErdosProblems.«421»
-import FormalConjectures.ErdosProblems.«422»
-import FormalConjectures.ErdosProblems.«424»
-import FormalConjectures.ErdosProblems.«427»
-import FormalConjectures.ErdosProblems.«428»
-import FormalConjectures.ErdosProblems.«42»
-import FormalConjectures.ErdosProblems.«434»
-import FormalConjectures.ErdosProblems.«442»
-import FormalConjectures.ErdosProblems.«44»
-import FormalConjectures.ErdosProblems.«454»
-import FormalConjectures.ErdosProblems.«455»
-import FormalConjectures.ErdosProblems.«457»
-import FormalConjectures.ErdosProblems.«458»
-import FormalConjectures.ErdosProblems.«463»
-import FormalConjectures.ErdosProblems.«469»
-import FormalConjectures.ErdosProblems.«470»
-import FormalConjectures.ErdosProblems.«477»
-import FormalConjectures.ErdosProblems.«479»
-import FormalConjectures.ErdosProblems.«480»
-import FormalConjectures.ErdosProblems.«486»
-import FormalConjectures.ErdosProblems.«488»
-import FormalConjectures.ErdosProblems.«489»
-import FormalConjectures.ErdosProblems.«48»
-import FormalConjectures.ErdosProblems.«494»
-import FormalConjectures.ErdosProblems.«495»
-import FormalConjectures.ErdosProblems.«499»
-import FormalConjectures.ErdosProblems.«4»
-import FormalConjectures.ErdosProblems.«503»
-import FormalConjectures.ErdosProblems.«507»
-import FormalConjectures.ErdosProblems.«508»
-import FormalConjectures.ErdosProblems.«509»
-import FormalConjectures.ErdosProblems.«510»
-import FormalConjectures.ErdosProblems.«513»
-import FormalConjectures.ErdosProblems.«516»
-import FormalConjectures.ErdosProblems.«517»
-import FormalConjectures.ErdosProblems.«51»
-import FormalConjectures.ErdosProblems.«520»
-import FormalConjectures.ErdosProblems.«522»
-import FormalConjectures.ErdosProblems.«536»
-import FormalConjectures.ErdosProblems.«541»
-import FormalConjectures.ErdosProblems.«562»
-import FormalConjectures.ErdosProblems.«564»
-import FormalConjectures.ErdosProblems.«566»
-import FormalConjectures.ErdosProblems.«567»
-import FormalConjectures.ErdosProblems.«56»
-import FormalConjectures.ErdosProblems.«587»
-import FormalConjectures.ErdosProblems.«590»
-import FormalConjectures.ErdosProblems.«591»
-import FormalConjectures.ErdosProblems.«592»
-import FormalConjectures.ErdosProblems.«598»
-import FormalConjectures.ErdosProblems.«617»
-import FormalConjectures.ErdosProblems.«61»
-import FormalConjectures.ErdosProblems.«623»
-import FormalConjectures.ErdosProblems.«624»
-import FormalConjectures.ErdosProblems.«645»
-import FormalConjectures.ErdosProblems.«647»
-import FormalConjectures.ErdosProblems.«64»
-import FormalConjectures.ErdosProblems.«659»
-import FormalConjectures.ErdosProblems.«66»
-import FormalConjectures.ErdosProblems.«672»
-import FormalConjectures.ErdosProblems.«677»
-import FormalConjectures.ErdosProblems.«678»
-import FormalConjectures.ErdosProblems.«67»
-import FormalConjectures.ErdosProblems.«680»
-import FormalConjectures.ErdosProblems.«681»
-import FormalConjectures.ErdosProblems.«686»
-import FormalConjectures.ErdosProblems.«689»
-import FormalConjectures.ErdosProblems.«68»
-import FormalConjectures.ErdosProblems.«694»
-import FormalConjectures.ErdosProblems.«695»
-import FormalConjectures.ErdosProblems.«697»
-import FormalConjectures.ErdosProblems.«699»
-import FormalConjectures.ErdosProblems.«69»
-import FormalConjectures.ErdosProblems.«6»
-import FormalConjectures.ErdosProblems.«705»
-import FormalConjectures.ErdosProblems.«707»
-import FormalConjectures.ErdosProblems.«723»
-import FormalConjectures.ErdosProblems.«727»
-import FormalConjectures.ErdosProblems.«728»
-import FormalConjectures.ErdosProblems.«730»
-import FormalConjectures.ErdosProblems.«741»
-import FormalConjectures.ErdosProblems.«749»
-import FormalConjectures.ErdosProblems.«74»
-import FormalConjectures.ErdosProblems.«757»
-import FormalConjectures.ErdosProblems.«770»
-import FormalConjectures.ErdosProblems.«779»
-import FormalConjectures.ErdosProblems.«786»
-import FormalConjectures.ErdosProblems.«817»
-import FormalConjectures.ErdosProblems.«822»
-import FormalConjectures.ErdosProblems.«825»
-import FormalConjectures.ErdosProblems.«826»
-import FormalConjectures.ErdosProblems.«828»
-import FormalConjectures.ErdosProblems.«82»
-import FormalConjectures.ErdosProblems.«830»
-import FormalConjectures.ErdosProblems.«835»
-import FormalConjectures.ErdosProblems.«845»
-import FormalConjectures.ErdosProblems.«846»
-import FormalConjectures.ErdosProblems.«847»
-import FormalConjectures.ErdosProblems.«848»
-import FormalConjectures.ErdosProblems.«849»
-import FormalConjectures.ErdosProblems.«850»
-import FormalConjectures.ErdosProblems.«851»
-import FormalConjectures.ErdosProblems.«853»
-import FormalConjectures.ErdosProblems.«855»
-import FormalConjectures.ErdosProblems.«859»
-import FormalConjectures.ErdosProblems.«85»
-import FormalConjectures.ErdosProblems.«865»
-import FormalConjectures.ErdosProblems.«868»
-import FormalConjectures.ErdosProblems.«873»
-import FormalConjectures.ErdosProblems.«881»
-import FormalConjectures.ErdosProblems.«885»
-import FormalConjectures.ErdosProblems.«886»
-import FormalConjectures.ErdosProblems.«887»
-import FormalConjectures.ErdosProblems.«888»
-import FormalConjectures.ErdosProblems.«889»
-import FormalConjectures.ErdosProblems.«890»
-import FormalConjectures.ErdosProblems.«891»
-import FormalConjectures.ErdosProblems.«893»
-import FormalConjectures.ErdosProblems.«897»
-import FormalConjectures.ErdosProblems.«899»
-import FormalConjectures.ErdosProblems.«89»
-import FormalConjectures.ErdosProblems.«906»
-import FormalConjectures.ErdosProblems.«90»
-import FormalConjectures.ErdosProblems.«912»
-import FormalConjectures.ErdosProblems.«913»
-import FormalConjectures.ErdosProblems.«918»
-import FormalConjectures.ErdosProblems.«920»
-import FormalConjectures.ErdosProblems.«92»
-import FormalConjectures.ErdosProblems.«930»
-import FormalConjectures.ErdosProblems.«931»
-import FormalConjectures.ErdosProblems.«932»
-import FormalConjectures.ErdosProblems.«936»
-import FormalConjectures.ErdosProblems.«938»
-import FormalConjectures.ErdosProblems.«939»
-import FormalConjectures.ErdosProblems.«940»
-import FormalConjectures.ErdosProblems.«942»
-import FormalConjectures.ErdosProblems.«943»
-import FormalConjectures.ErdosProblems.«944»
-import FormalConjectures.ErdosProblems.«945»
-import FormalConjectures.ErdosProblems.«946»
-import FormalConjectures.ErdosProblems.«949»
-import FormalConjectures.ErdosProblems.«951»
-import FormalConjectures.ErdosProblems.«952»
-import FormalConjectures.ErdosProblems.«961»
-import FormalConjectures.ErdosProblems.«965»
-import FormalConjectures.ErdosProblems.«968»
-import FormalConjectures.ErdosProblems.«971»
-import FormalConjectures.ErdosProblems.«972»
-import FormalConjectures.ErdosProblems.«975»
-import FormalConjectures.ErdosProblems.«978»
-import FormalConjectures.ErdosProblems.«979»
-import FormalConjectures.ErdosProblems.«97»
-import FormalConjectures.ErdosProblems.«982»
-import FormalConjectures.ErdosProblems.«985»
-import FormalConjectures.ErdosProblems.«996»
-import FormalConjectures.ErdosProblems.«997»
-import FormalConjectures.ErdosProblems.«99»
-import FormalConjectures.ErdosProblems.«9»
-import FormalConjectures.GreensOpenProblems.«12»
-import FormalConjectures.GreensOpenProblems.«15»
-import FormalConjectures.GreensOpenProblems.«16»
-import FormalConjectures.GreensOpenProblems.«18»
-import FormalConjectures.GreensOpenProblems.«19»
-import FormalConjectures.GreensOpenProblems.«1»
-import FormalConjectures.GreensOpenProblems.«23»
-import FormalConjectures.GreensOpenProblems.«24»
-import FormalConjectures.GreensOpenProblems.«26»
-import FormalConjectures.GreensOpenProblems.«2»
-import FormalConjectures.GreensOpenProblems.«35»
-import FormalConjectures.GreensOpenProblems.«37»
-import FormalConjectures.GreensOpenProblems.«3»
-import FormalConjectures.GreensOpenProblems.«45»
-import FormalConjectures.GreensOpenProblems.«4»
-import FormalConjectures.GreensOpenProblems.«57»
-import FormalConjectures.GreensOpenProblems.«58»
-import FormalConjectures.GreensOpenProblems.«60»
-import FormalConjectures.GreensOpenProblems.«61»
-import FormalConjectures.GreensOpenProblems.«62»
-import FormalConjectures.GreensOpenProblems.«63»
-import FormalConjectures.GreensOpenProblems.«72»
-import FormalConjectures.GreensOpenProblems.«77»
-import FormalConjectures.GreensOpenProblems.«7»
-import FormalConjectures.GreensOpenProblems.«81»
-import FormalConjectures.GreensOpenProblems.«85»
-import FormalConjectures.GreensOpenProblems.«94»
-import FormalConjectures.GreensOpenProblems.«9»
-import FormalConjectures.HilbertProblems.«17»
-import FormalConjectures.Kourovka.«19_25»
-import FormalConjectures.Kourovka.«20_76»
-import FormalConjectures.Mathoverflow.«1973»
-import FormalConjectures.Mathoverflow.«21003»
-import FormalConjectures.Mathoverflow.«235893»
-import FormalConjectures.Mathoverflow.«31809»
-import FormalConjectures.Mathoverflow.«339137»
-import FormalConjectures.Mathoverflow.«34145»
-import FormalConjectures.Mathoverflow.«347178»
-import FormalConjectures.Mathoverflow.«486451»
-import FormalConjectures.Mathoverflow.«75792»
-import FormalConjectures.Millenium.GeneralizedRiemannHypothesis
-import FormalConjectures.Millenium.PvsNP
-import FormalConjectures.OEIS.«228828»
-import FormalConjectures.OEIS.«231201»
-import FormalConjectures.OEIS.«232174»
-import FormalConjectures.OEIS.«239957»
-import FormalConjectures.OEIS.«280831»
-import FormalConjectures.OEIS.«281976»
-import FormalConjectures.OEIS.«287616»
-import FormalConjectures.OEIS.«303656»
-import FormalConjectures.OEIS.«306477»
-import FormalConjectures.OEIS.«308734»
-import FormalConjectures.OEIS.«34693»
-import FormalConjectures.OEIS.«358684»
-import FormalConjectures.OEIS.«41»
-import FormalConjectures.OEIS.«56777»
-import FormalConjectures.OEIS.«63880»
-import FormalConjectures.OEIS.«6697»
-import FormalConjectures.OEIS.«67720»
-import FormalConjectures.OEIS.«80170»
-import FormalConjectures.OEIS.«81091»
-import FormalConjectures.OEIS.«87719»
-import FormalConjectures.Other.BeaverMathOlympiad
-import FormalConjectures.Other.EquationalTheories_677_255
-import FormalConjectures.Other.SchurTruncatedExponential
-import FormalConjectures.Other.VCDimConvex
-import FormalConjectures.Paper.CardinalityLindelof
-import FormalConjectures.Paper.CasasAlvero
-import FormalConjectures.Paper.CatchUpConjecture
-import FormalConjectures.Paper.Chvatal
-import FormalConjectures.Paper.DegreeSequencesTriangleFree
-import FormalConjectures.Paper.Gourevitch
-import FormalConjectures.Paper.HartshorneConjecture
-import FormalConjectures.Paper.Homogenous
-import FormalConjectures.Paper.Kurepa
-import FormalConjectures.Paper.LatinTableau
-import FormalConjectures.Paper.PrimeTuples
-import FormalConjectures.Paper.Rupert
-import FormalConjectures.Paper.StrongSensitivityConjecture
-import FormalConjectures.Paper.WeaklyFirstCountable
-import FormalConjectures.Util.Answer
-import FormalConjectures.Util.Answer.Syntax
-import FormalConjectures.Util.Attributes.AMS
-import FormalConjectures.Util.Attributes.Basic
-import FormalConjectures.Util.ForMathlib
-import FormalConjectures.Util.Linters.AMSLinter
-import FormalConjectures.Util.Linters.AnswerLinter
-import FormalConjectures.Util.Linters.AnswerLinterTest
-import FormalConjectures.Util.Linters.CategoryLinter
-import FormalConjectures.Util.Linters.CopyrightLinter
-import FormalConjectures.Util.Linters.NamespaceLinter
-import FormalConjectures.Util.ProblemImports
-import FormalConjectures.Wikipedia.ABC
-import FormalConjectures.Wikipedia.AgohGiuga
-import FormalConjectures.Wikipedia.Andrica
-import FormalConjectures.Wikipedia.ArtinPrimitiveRootsConjecture
-import FormalConjectures.Wikipedia.BalancedPrimes
-import FormalConjectures.Wikipedia.BatemanHornConjecture
-import FormalConjectures.Wikipedia.BealConjecture
-import FormalConjectures.Wikipedia.BetrothedNumbers
-import FormalConjectures.Wikipedia.BoundedBurnsideProblem
-import FormalConjectures.Wikipedia.BrocardConjecture
-import FormalConjectures.Wikipedia.BrocardProblem
-import FormalConjectures.Wikipedia.Bunyakovsky
-import FormalConjectures.Wikipedia.BusyBeaver
-import FormalConjectures.Wikipedia.CarmichaelTotient
-import FormalConjectures.Wikipedia.Catalan
-import FormalConjectures.Wikipedia.ClassNumberProblem
-import FormalConjectures.Wikipedia.CollatzConjecture
-import FormalConjectures.Wikipedia.CongruentNumber
-import FormalConjectures.Wikipedia.Conway99Graph
-import FormalConjectures.Wikipedia.DeterminantalConjecture
-import FormalConjectures.Wikipedia.Dickson
-import FormalConjectures.Wikipedia.EllipticCurveRank
-import FormalConjectures.Wikipedia.Euclid
-import FormalConjectures.Wikipedia.EulerBrick
-import FormalConjectures.Wikipedia.EulerSumOfPowers
-import FormalConjectures.Wikipedia.Exponentials
-import FormalConjectures.Wikipedia.FeitThompsonPrimeConjecture
-import FormalConjectures.Wikipedia.Fermat
-import FormalConjectures.Wikipedia.FermatCatalanConjecture
-import FormalConjectures.Wikipedia.FibonacciPrimes
-import FormalConjectures.Wikipedia.Firoozbakht
-import FormalConjectures.Wikipedia.GaussCircleProblem
-import FormalConjectures.Wikipedia.Gilbreath
-import FormalConjectures.Wikipedia.GoldbachConjecture
-import FormalConjectures.Wikipedia.Grimm
-import FormalConjectures.Wikipedia.GromovPolynomialGrowth
-import FormalConjectures.Wikipedia.Hadamard
-import FormalConjectures.Wikipedia.HadwigerNelson
-import FormalConjectures.Wikipedia.Hall
-import FormalConjectures.Wikipedia.HappyEndingProblem
-import FormalConjectures.Wikipedia.HardyLittlewood
-import FormalConjectures.Wikipedia.HerzogSchonheimConjecture
-import FormalConjectures.Wikipedia.InscribedSquare
-import FormalConjectures.Wikipedia.InvariantSubspaceProblem
-import FormalConjectures.Wikipedia.InverseGalois
-import FormalConjectures.Wikipedia.Irrational
-import FormalConjectures.Wikipedia.JacobianConjecture
-import FormalConjectures.Wikipedia.JugglerConjecture
-import FormalConjectures.Wikipedia.Kakeya
-import FormalConjectures.Wikipedia.Kaplansky
-import FormalConjectures.Wikipedia.Koethe
-import FormalConjectures.Wikipedia.KummerVandiver
-import FormalConjectures.Wikipedia.LegendreConjecture
-import FormalConjectures.Wikipedia.LehmerMahlerMeasureProblem
-import FormalConjectures.Wikipedia.LehmerTotient
-import FormalConjectures.Wikipedia.LeinsterGroup
-import FormalConjectures.Wikipedia.Lemoine
-import FormalConjectures.Wikipedia.LittlewoodConjecture
-import FormalConjectures.Wikipedia.LonelyRunnerConjecture
-import FormalConjectures.Wikipedia.MagicSquareOfSquares
-import FormalConjectures.Wikipedia.Mahler32
-import FormalConjectures.Wikipedia.Mandelbrot
-import FormalConjectures.Wikipedia.MeanValueProblem
-import FormalConjectures.Wikipedia.Mersenne
-import FormalConjectures.Wikipedia.MinimalOverlapProblem
-import FormalConjectures.Wikipedia.ModularityConjecture
-import FormalConjectures.Wikipedia.MoserWorm
-import FormalConjectures.Wikipedia.NoetherProblem
-import FormalConjectures.Wikipedia.Oppermann
-import FormalConjectures.Wikipedia.PebblingNumberConjecture
-import FormalConjectures.Wikipedia.Pell
-import FormalConjectures.Wikipedia.PerfectNumbers
-import FormalConjectures.Wikipedia.PierceBirkhoff
-import FormalConjectures.Wikipedia.PollocksConjecture
-import FormalConjectures.Wikipedia.PrimesAndPerfectSquares
-import FormalConjectures.Wikipedia.RamanujanTau
-import FormalConjectures.Wikipedia.RationalDistanceProblem
-import FormalConjectures.Wikipedia.RegularPrimes
-import FormalConjectures.Wikipedia.RiemannZetaValues
-import FormalConjectures.Wikipedia.Schanuel
-import FormalConjectures.Wikipedia.Schinzel
-import FormalConjectures.Wikipedia.Selfridge
-import FormalConjectures.Wikipedia.Sendov
-import FormalConjectures.Wikipedia.Singmaster
-import FormalConjectures.Wikipedia.SnakeInTheBox
-import FormalConjectures.Wikipedia.SparseRuler
-import FormalConjectures.Wikipedia.SquarePacking
-import FormalConjectures.Wikipedia.SumOfThreeCubes
-import FormalConjectures.Wikipedia.Toronto
-import FormalConjectures.Wikipedia.Transcendental
-import FormalConjectures.Wikipedia.TwinPrimes
-import FormalConjectures.Wikipedia.UnionClosed
-import FormalConjectures.Wikipedia.VaughtConjecture
-import FormalConjectures.Wikipedia.WallSunSun
-import FormalConjectures.Wikipedia.WolstenholmePrime
-import FormalConjectures.Wikipedia.WoodalPrimes
-import FormalConjectures.Wikipedia.conjecture_1_3_to_2_3
-import FormalConjectures.WrittenOnTheWallII.GraphConjecture1
-import FormalConjectures.WrittenOnTheWallII.GraphConjecture19
-import FormalConjectures.WrittenOnTheWallII.GraphConjecture2
-import FormalConjectures.WrittenOnTheWallII.GraphConjecture3
-import FormalConjectures.WrittenOnTheWallII.GraphConjecture34
-import FormalConjectures.WrittenOnTheWallII.GraphConjecture4
-import FormalConjectures.WrittenOnTheWallII.GraphConjecture40
-import FormalConjectures.WrittenOnTheWallII.GraphConjecture5
-import FormalConjectures.WrittenOnTheWallII.GraphConjecture58
-import FormalConjectures.WrittenOnTheWallII.GraphConjecture6
-import FormalConjectures.WrittenOnTheWallII.Test
diff --git a/Benchmarks/CompileFC/README.md b/Benchmarks/CompileFC/README.md
deleted file mode 100644
index c10070222..000000000
--- a/Benchmarks/CompileFC/README.md
+++ /dev/null
@@ -1,19 +0,0 @@
-# CompileFC
-
-Runs the Ix compiler over the Lean environment of all defs from https://github.com/google-deepmind/formal-conjectures.
-
-The defs in CompileFC.lean were generated automatically with the following:
-```
-lake update
-cd .lake/packages/formal_conjectures
-lake exe mk_all --lib FormalConjectures
-mv FormalConjectures.lean ../../../CompileFC.lean
-```
-
-This project shadows the `formal-conjectures` project's Lean version, which is not always up to date.
-
-## Usage
-
-First ensure the Lean version used to build Ix matches the `Benchmarks/CompileFC/lean-toolchain` version (check against `ix --version`). Then run
-
-`ix compile /path/to/CompileFC.lean`
diff --git a/Benchmarks/CompileFC/flake.lock b/Benchmarks/CompileFC/flake.lock
deleted file mode 100644
index e2d0ab18f..000000000
--- a/Benchmarks/CompileFC/flake.lock
+++ /dev/null
@@ -1,117 +0,0 @@
-{
-  "nodes": {
-    "flake-parts": {
-      "inputs": {
-        "nixpkgs-lib": "nixpkgs-lib"
-      },
-      "locked": {
-        "lastModified": 1769996383,
-        "narHash": "sha256-AnYjnFWgS49RlqX7LrC4uA+sCCDBj0Ry/WOJ5XWAsa0=",
-        "owner": "hercules-ci",
-        "repo": "flake-parts",
-        "rev": "57928607ea566b5db3ad13af0e57e921e6b12381",
-        "type": "github"
-      },
-      "original": {
-        "owner": "hercules-ci",
-        "repo": "flake-parts",
-        "type": "github"
-      }
-    },
-    "flake-parts_2": {
-      "inputs": {
-        "nixpkgs-lib": "nixpkgs-lib_2"
-      },
-      "locked": {
-        "lastModified": 1765835352,
-        "narHash": "sha256-XswHlK/Qtjasvhd1nOa1e8MgZ8GS//jBoTqWtrS1Giw=",
-        "owner": "hercules-ci",
-        "repo": "flake-parts",
-        "rev": "a34fae9c08a15ad73f295041fec82323541400a9",
-        "type": "github"
-      },
-      "original": {
-        "owner": "hercules-ci",
-        "repo": "flake-parts",
-        "type": "github"
-      }
-    },
-    "lean4-nix": {
-      "inputs": {
-        "flake-parts": "flake-parts_2",
-        "nixpkgs": "nixpkgs"
-      },
-      "locked": {
-        "lastModified": 1770601541,
-        "narHash": "sha256-wCun5wynV3vLoVrr9gU46qI0UG4YeID6IKhPIhtsp8U=",
-        "owner": "lenianiva",
-        "repo": "lean4-nix",
-        "rev": "561f1a779737e109d4e03a6f967108497bbbd73f",
-        "type": "github"
-      },
-      "original": {
-        "owner": "lenianiva",
-        "repo": "lean4-nix",
-        "type": "github"
-      }
-    },
-    "nixpkgs": {
-      "locked": {
-        "lastModified": 1765779637,
-        "narHash": "sha256-KJ2wa/BLSrTqDjbfyNx70ov/HdgNBCBBSQP3BIzKnv4=",
-        "owner": "nixos",
-        "repo": "nixpkgs",
-        "rev": "1306659b587dc277866c7b69eb97e5f07864d8c4",
-        "type": "github"
-      },
-      "original": {
-        "owner": "nixos",
-        "ref": "nixos-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
-    "nixpkgs-lib": {
-      "locked": {
-        "lastModified": 1769909678,
-        "narHash": "sha256-cBEymOf4/o3FD5AZnzC3J9hLbiZ+QDT/KDuyHXVJOpM=",
-        "owner": "nix-community",
-        "repo": "nixpkgs.lib",
-        "rev": "72716169fe93074c333e8d0173151350670b824c",
-        "type": "github"
-      },
-      "original": {
-        "owner": "nix-community",
-        "repo": "nixpkgs.lib",
-        "type": "github"
-      }
-    },
-    "nixpkgs-lib_2": {
-      "locked": {
-        "lastModified": 1765674936,
-        "narHash": "sha256-k00uTP4JNfmejrCLJOwdObYC9jHRrr/5M/a/8L2EIdo=",
-        "owner": "nix-community",
-        "repo": "nixpkgs.lib",
-        "rev": "2075416fcb47225d9b68ac469a5c4801a9c4dd85",
-        "type": "github"
-      },
-      "original": {
-        "owner": "nix-community",
-        "repo": "nixpkgs.lib",
-        "type": "github"
-      }
-    },
-    "root": {
-      "inputs": {
-        "flake-parts": "flake-parts",
-        "lean4-nix": "lean4-nix",
-        "nixpkgs": [
-          "lean4-nix",
-          "nixpkgs"
-        ]
-      }
-    }
-  },
-  "root": "root",
-  "version": 7
-}
diff --git a/Benchmarks/CompileFC/flake.nix b/Benchmarks/CompileFC/flake.nix
deleted file mode 100644
index 57b04053c..000000000
--- a/Benchmarks/CompileFC/flake.nix
+++ /dev/null
@@ -1,53 +0,0 @@
-{
-  description = "Ix Nix flake (Lean4 + C + Rust)";
-
-  inputs = {
-    # System packages, follows lean4-nix so we stay in sync
-    nixpkgs.follows = "lean4-nix/nixpkgs";
-
-    # Lean 4 & Lake
-    lean4-nix.url = "github:lenianiva/lean4-nix";
-
-    # Helper: flake-parts for easier outputs
-    flake-parts.url = "github:hercules-ci/flake-parts";
-  };
-
-  outputs = inputs @ {
-    nixpkgs,
-    flake-parts,
-    lean4-nix,
-    ...
-  }:
-    flake-parts.lib.mkFlake {inherit inputs;} {
-      # Systems we want to build for
-      systems = [
-        "aarch64-darwin"
-        "aarch64-linux"
-        "x86_64-darwin"
-        "x86_64-linux"
-      ];
-
-      perSystem = {
-        system,
-        pkgs,
-        ...
-      }: {
-        # Lean overlay
-        _module.args.pkgs = import nixpkgs {
-          inherit system;
-          overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
-        };
-        # Provide a unified dev shell with Lean + Rust
-        devShells.default = pkgs.mkShell {
-          packages = with pkgs; [
-            pkg-config
-            openssl
-            clang
-            lean.lean-all # Includes Lean compiler, lake, stdlib, etc.
-          ];
-        };
-
-        formatter = pkgs.alejandra;
-      };
-    };
-}
diff --git a/Benchmarks/CompileFC/lake-manifest.json b/Benchmarks/CompileFC/lake-manifest.json
deleted file mode 100644
index c386f41a0..000000000
--- a/Benchmarks/CompileFC/lake-manifest.json
+++ /dev/null
@@ -1,105 +0,0 @@
-{"version": "1.1.0",
- "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/google-deepmind/formal-conjectures",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "bfe92e43cf56f4fb5fe1a9fac0fc093acf4f88ea",
-   "name": "formal_conjectures",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "bfe92e43cf56f4fb5fe1a9fac0fc093acf4f88ea",
-   "inherited": false,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900",
-   "name": "mathlib",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/plausible",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f",
-   "name": "plausible",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/LeanSearchClient",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
-   "name": "LeanSearchClient",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2",
-   "name": "importGraph",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "c04225ee7c0585effbd933662b3151f01b600e40",
-   "name": "proofwidgets",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.85",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
-   "name": "aesop",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/quote4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
-   "name": "Qq",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/batteries",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
-   "name": "batteries",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "55c37290ff6186e2e965d68cf853a57c0702db82",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
-   "inherited": true,
-   "configFile": "lakefile.toml"}],
- "name": "CompileFC",
- "lakeDir": ".lake"}
diff --git a/Benchmarks/CompileFC/lakefile.toml b/Benchmarks/CompileFC/lakefile.toml
deleted file mode 100644
index 2536d3750..000000000
--- a/Benchmarks/CompileFC/lakefile.toml
+++ /dev/null
@@ -1,11 +0,0 @@
-name = "CompileFC"
-version = "0.1.0"
-defaultTargets = ["CompileFC"]
-
-[[lean_lib]]
-name = "CompileFC"
-
-[[require]]
-name = "formal_conjectures"
-git = "https://github.com/google-deepmind/formal-conjectures"
-rev = "bfe92e43cf56f4fb5fe1a9fac0fc093acf4f88ea"
diff --git a/Benchmarks/CompileFC/lean-toolchain b/Benchmarks/CompileFC/lean-toolchain
deleted file mode 100644
index 5249182c0..000000000
--- a/Benchmarks/CompileFC/lean-toolchain
+++ /dev/null
@@ -1 +0,0 @@
-leanprover/lean4:v4.27.0