A software that assists a previous version of the proof of Gerver's conjecture, using a custom geometric branch-and-bound algorithm, and the exact rational QP solver powered by CGAL
-
Updated
Apr 3, 2024 - C++
A software that assists a previous version of the proof of Gerver's conjecture, using a custom geometric branch-and-bound algorithm, and the exact rational QP solver powered by CGAL
Discrete Kakeya cover for LLM KV cache: D4/E8 nested-lattice quantisation realising a Kakeya-style tube-cover over the direction sphere. 2.4x-2.8x compression at <1% perplexity loss on Qwen3, Llama-3, DeepSeek, GLM-4, Gemma. Drop-in transformers.DynamicCache. pip install kakeyalattice.
This repository is associated with the paper: “A Poset-Based Approach to Curvature of Hypergraphs”
Disk covering problem (disc covering): global optimality proof claims for n = 11-20, exact certificates, Chinese proofs, and reproducible verification code. External review pending.
A Codex research workbench for discrete geometry and geometric analysis
Tracing curve on 2D plane = drawing curve on complex (2D) plane. Curve is a field line or equipotential line of potential scalar field.
An SAT encoding of Erdős-Szekeres conjecture, including counterexamples of its variants
Solver for realizability of pseudo-points (through CC-systems / signotopes / triple orientations).
tc18.org web site (https://www.tc18.org)
Certified unit-distance point sets and graphs for discrete geometry in Rust.
lean theorems
Implements digitized transformations defined in the space with geometric algebra (mostly Klein lib).
Geometric-Electromagnetic Model (GEM): A topological reformulation of the quantum vacuum as a Riemann-Cartan manifold with icosahedral substructure. Includes the published paper (DOI: 10.5281/zenodo.21268209), foundational documents, and experimental protocols.
Lean 4 proof of the dimension-five variants of Erdős problem 1007: the least edge count of a graph of dimension five is 15, attained by K₆ and K₁,₃,₃.
A Lean 4 Certified Proof of 3D Aperiodic Monotiles by Triviality of the Projection Kernel.
Lean 4 proof of the extremal half of Erdős problem 1007: a graph of dimension four with nine edges and no isolated vertex is K₃,₃.
Independent Python reproduction of the 2026 OpenAI/Sawin disproof of the Erdős unit-distance conjecture. mpmath-200-bit verbatim match (0.01% rel.err) to equation (2.2) of the remarks PDF. MIT, NumPy + mpmath only.
Новые верхние оценки хроматических чисел евклидовых пространств: χ(ℝ⁴)≤43, χ(ℝ⁵)≤132, χ(ℝ⁷)≤1029, χ(ℝ⁹)≤7203, χ(ℝ¹⁰)≤45619 — код, точные сертификаты и статьи
Code for publication: Hypergraph Geometry Reflects Higher-Order Dynamics in Protein Interaction Networks; Kevin A. Murgas, Emil Saucan, Romeil Sandhu; Scientific Reports (2022)
Rigorous bounds and reproducible certificates for covering the unit disk with 100 equal disks, with constructions, local results and failed routes; the global optimum remains open.
To associate your repository with the discrete-geometry topic, visit your repo's landing page and select "manage topics."