| module | |
| import Lean | |
| meta import Lean | |
| /-! Population-count replay comparison; standalone timings are enabled with POPCOUNT_SAMPLES. | |
| The current API and alternative chunk widths count identical numeral inputs. -/ | |
| open Lean | |
| @[expose] public def countBits (n : Nat) : Nat → Nat := | |
| Nat.rec 0 (fun i acc => acc + (n.testBit i).toNat) |
| module | |
| import Lean | |
| meta import Lean | |
| /-! Population-count replay comparison; standalone timings are enabled with POPCOUNT_SAMPLES. | |
| The old BitVec bit loop and the Nat primitive count identical numeral inputs. -/ | |
| open Lean | |
| @[expose] public def countBits (n : Nat) : Nat → Nat := | |
| Nat.rec 0 (fun i acc => acc + (n.testBit i).toNat) |
| /- | |
| Copyright (c) 2026 Lean FRO, LLC. All rights reserved. | |
| Released under Apache 2.0 license as described in the file LICENSE. | |
| Authors: Kim Morrison | |
| -/ | |
| module | |
| public import PrimeCert | |
| public import PrimeCert.SieveBase | |
| public meta import PrimeCert.Meta.SieveLookup |
| module | |
| import Lean | |
| import PrimeCert.Pocklington3 | |
| meta import Lean | |
| open Lean | |
| set_option maxRecDepth 10000 | |
| run_cmd do | |
| let ready ← IO.mkRef (← getEnv).toKernelEnv | |
| let env := Environment.ofKernelEnv (← ready.get) |
The implementation uses windows of 6, 4, 3, and 2 bits through moduli
2^64, 2^512, 2^1024, and 2^2048. Above that, reduced bases below
2^64 use two bits through 2^4096, then one bit. Other bases use binary.
There is no exponent-length cutoff.
Implement the full lifecycle overhaul through production rollout: immutable v1, problem lifecycle metadata, results schema version 2, append-only state, replay and kernel validation, a Cloudflare submission server, automatic publication, the lifecycle-aware leaderboard, generator extraction, software verification, FC100 integration, and later comparator disproof support.
Terminology: unqualified v1 and v2 refer only to problem sets. This program calls the platform work the lifecycle overhaul, and the resulting system the lifecycle-aware platform. Versioned machine formats are always qualified, for example results schema version 2; frozen identifiers and
| import Mathlib.Data.Real.Basic | |
| import EvalTools.Markers | |
| /-! | |
| # Quantifier elimination for real closed fields | |
| ## The task | |
| Work in the first-order language of ordered rings: `Term`s are built from variables, integer | |
| constants, `+`, `*` and `-`, and `Formula`s are built from the atoms `<` and `=` using `⊥`, `→` |
| import EvalTools.Markers | |
| /-! | |
| # Strong normalization for the calculus of constructions with universes | |
| ## The system | |
| `Tm` is the usual lambda syntax with de Bruijn variables: variables, sorts, application, | |
| `lam A b` for `λ (x : A). b`, and `pi A B` for `Π (x : A). B`. The sorts `Srt` are an | |
| impredicative `Prop` together with a predicative hierarchy `Type 0`, `Type 1`, ..., typed by |
A skeptical review of the $LAKE_WRAPPED_EXEC hook, cross-checked by Claude (Opus 4.8) and OpenAI Codex. Both read the PR branch directly; every concern below was independently confirmed against the code.
Build/Actions.lean refactor is behavior-preserving. mkLeanModuleArgs / mkCcCompileArgs preserve argv order, escapeRspArg is the same escaping factored out, and compileLeanModule keeps the same createParentDirs calls.runRawProcOrWrapped falls through to rawProc with the same logging.
| #!/usr/bin/env python3 | |
| """ | |
| Reproducer for mathlib4 PR #40110 — linarith atomization speedup. | |
| Generates two Lean files (Bench80.lean, Bench160.lean) that each call | |
| `linarith (config := {})` several times on a dense rational LP: | |
| 0 ≤ xᵢ, xᵢ ≤ 1, Σxᵢ ≤ n | |
| with n distinct atoms and 2n bound hypotheses. | |
| Usage |