Independent research lab · New York
Lobsenz Research works where number theory, formal verification, and the science of large language models meet. We publish proofs, study how models reason, and build AI systems that hold up in production.
Research programs
We work on problems where getting the details right is the whole point: theorems that are machine-checked, model analyses that are causal rather than correlational, and systems with measured performance.
Why do some language models reason better than others? We look inside open-weight models to find the internal operations that working memory and abstract reasoning share.
When lines of sight bend into polynomial curves, which lattice points stay visible? Three 2026 papers settle the Visibility Density Conjecture for nonzero polynomials.
Frontier models are now useful collaborators in proof discovery. We pair them with the Lean proof assistant, so every claimed theorem is verified end to end by a small trusted kernel.
Capable models running on hardware you control: speculative decoding, KV-cache engineering, and tool-using agents with built-in checks on their own claims.
Latest result · September 2026
Lattice points that are visible along straight lines thin out to a density of 6/π². Along polynomial curves, the picture changes. This paper proves that every nonzero integer polynomial with at least two distinct roots has visibility density one, resolving the generalized form of the Visibility Density Conjecture for nonzero polynomials. The proof is elementary, short, and verified line by line in Lean.
example (F : Polynomial ℤ) (hF : F ≠ 0) (hroots : ∃ z w : ℂ, z ≠ w ∧ F.aeval z = 0 ∧ F.aeval w = 0) : Filter.Tendsto (fun N : ℕ => (visibleCount F N : ℝ) / (N : ℝ)^2) Filter.atTop (nhds 1) := visibility_density_one F hF hroots #print axioms visibility_density_one -- [propext, Classical.choice, Quot.sound]
Applied AI
Our applied practice builds LLM systems, automation, and quantitative tools for organizations, and measures them the way we measure our research.
A native macOS system that files email and attachments into the firm's practice-management platform (Clio) from Apple Mail in one keystroke, and also logs time and creates tasks. Built on OAuth, an incremental SQLite/FTS5 sync engine, and an offline retry queue.
In daily production use. Large-file mail sync is 2–3× faster after a re-platforming.
qwen-harness serves a 35B mixture-of-experts model as a tool-calling agent on Apple Silicon, with speculative decoding, KV-cache engineering, and an audit gate that verifies numeric claims against tool outputs.
+37–45% decode throughput on long prompts. Open source.
CAP segments microscopy images to measure what fraction of a plate is covered by cells, with JIT-compiled post-processing and parallel batch analysis behind an interface built for bench scientists.
Used by a USC lab for 2+ years · 440+ downloads · cited.
Notes
Long-form technical notes with full derivations and working code, from number theory to optimization.
A plain-language companion to our arXiv paper with Tristan Phillips, and to the two papers that followed: what happens to visibility when lines of sight bend into curves.
The workhorse of modern optimization, derived from first principles, with a from-scratch Python implementation of Adam.
A closed form for the ordered sum of cosine products, derived from the roots-of-unity factorization of odd powers.
Work with us
We take on a small number of research collaborations and applied-AI engagements at a time. Tell us what you're working on.