integer-mult-bounds

Bindwidth is a browser-based calculator for sizing on-premises LLM inference infrastructure and estimating total cost of ownership. It evaluates three constraints for a resident text model—KV-cache memory, combined prefill and decode serving capacity, and the runtime session ceiling—and identifies which constraint binds for a workload. The tool accounts for interactive users and autonomous agents as different load types, then compares owned hardware, eligible sovereign rentals, and enterprise subscriptions with per-token APIs for agents. It distinguishes measured from estimated hardware and model data through confidence levels and profile-specific overrides, flags domain and model-capability limits, and exports a decision record as Markdown or the full scenario as JSON. The repository describes it as a directional sensitivity estimator rather than a procurement quote. It is a frontend-only application with no build step, server, database, account, or telemetry; calculations run in the browser and entered data is not transmitted.

A research artifact containing a complete machine-checked Lean 4 proof of Fermat's Last Theorem, following the Frey–Serre–Ribet–Wiles and Taylor–Wiles argument and built on Mathlib. The theorem states that for natural numbers n, a, b, and c with n ≥ 3 and a, b, and c positive, a^n + b^n ≠ c^n. Lean's kernel checks the proof, which uses only Lean's three standard axioms—propext, Classical.choice, and Quot.sound—and the repository excludes sorry statements, added axioms, native_decide, unsafe code, and related escape mechanisms. A comparator independently replays the environment against a Mathlib formulation, while Nanoda, an independent Lean kernel implemented in Rust, checks an exported version of the environment. The repository also includes PROOF-PATH.md and an offline HTML presentation of the proof's theorems, definitions, dependencies, and generated documentation. It is released under the Apache License 2.0 and is described as not maintained and not accepting contributions.

An OpenAI repository containing Lean 4 formalizations of ten results presented in its paper on advances in mathematics and theoretical computer science. The formalizations cover high-dimensional sphere packing; binary and spherical codes; non-sofic groups; Connes’s rigidity conjecture; arithmetic circuit complexity; quantum parallel repetition; the closest vector problem; Ehrhart’s volume conjecture; multicolor Ramsey numbers; and compactness and degeneracy conjectures in extremal graph theory. Each result is implemented as a separate Lean module, including `SpherePacking.lean`, `MetricCodes.lean`, `NonSoficGroup.lean`, `ConnesRigidity.lean`, `Permanent.lean`, `QuantumParallelRepetition.lean`, `GapCVP.lean`, `EhrhartVolumeInequality.lean`, `MulticolorTriangleRamsey.lean`, and `CompactnessAndDegeneracy.lean`. The project uses Lean 4.32.0, mathlib, and Lake. With the mathlib cache installed, all formalizations can be built with `lake build All`, or individual modules can be built by name; the repository also provides reasoning walkthroughs and documents independent checking with Comparator.

edge0 is an open-source streaming Mixture-of-Experts inference framework for running sparse MoE models on Apple Silicon Macs. Its MLX backend memory-maps expert weights from SSD storage and loads them on demand, so peak memory depends on the active experts rather than the model's total parameter count. A trained prerouter predicts the next expert routes so storage reads can overlap the forward pass, while Recover-LoRA adapters distill from the full-precision model to compensate for quantization loss; the base weights remain read-only and the adapters stay separate. The framework ships two end-to-end model tiers with bundled 4-bit checkpoints, LoRA adapters, and prerouter heads. It provides a command-line interface and Python API, supports demo, chat, and server modes, and exposes an OpenAI-compatible `/v1/chat/completions` endpoint. The current backend supports macOS on Apple Silicon M1 through M4; CUDA support is identified as planned. The repository is licensed under Apache-2.0.

Interference Search is a research project and Python library for reasoning over explicit states rather than a single linear language-model transcript. It expands live branches in parallel, lets the environment execute their moves, merges branches that reach the same state, uses a trained judge to discard states unlikely to reach the goal, and advances the surviving frontier one level at a time. The method is classical and does not claim quantum speedup. The repository implements Countdown arithmetic search and program search, including move generation, exact solving, judge training, sandboxed program tests, behavioral merging, benchmarks, raw results, failed experiments, a research log, and the accompanying paper. Its reported experiments compare the approach with linear language-model reasoning and other search strategies; it also includes a one-line baseline and tools for reproducing the Countdown results. The package requires Python 3.10 or newer and runs with PyTorch. Language-model experiments use MLX on Apple silicon, while the core search, judge, and tests can run on other PyTorch-supported systems. It is distributed under the Apache 2.0 license.