Amit Aminov

About

I’m a data scientist and ML researcher with a physics foundation (B.Sc. through Bar-Ilan’s program for youth gifted in mathematics) and years of applied quantitative work. I led an Operations Research and Data Science team in Unit 8200 — hiring, mentoring, and shipping end-to-end ML pipelines — then built statistical models in the IAF’s Operations Research Branch, work recognized with the Israel Defense Prize. In my research M.Sc. at the Hebrew University I work on machine learning for formal reasoning: fine-tuning LLMs to prove theorems in Lean 4, where a verifier, not a leaderboard, decides what counts. Across all of it I build ML systems with careful evaluation, reproducible experiments, and statistically grounded analysis — I try not to trust a number until I understand how it was produced.

• 2024–Present IAF Operations Research Branch · Israel Defense Prize
• 2023–Present M.Sc. Computer Science (research), Hebrew University of Jerusalem
• 2022–2024 Unit 8200 · Operations Research & Data Science team lead
• 2018–2021 B.Sc. Physics, Bar-Ilan University (gifted-in-math program)

Featured projects

• 

  Generated Formal Theorem Proofs in Lean

  Goal-blind baselines that measure how much of a neural theorem prover’s success is reasoning versus corpus tactic frequency.

  Problem

  Neural provers are rarely compared against a simple baseline, so it’s unclear how much of their success comes from reasoning about the goal versus favoring tactics common in the training corpus.

  Method

  A goal-blind sampler that replays only Mathlib4 tactic frequencies — never reading the statement or proof state — run under the same best-first search budget as the neural prover.

  Result

  A 16,850-parameter frequency table clears 26.2% of miniF2F-test (64/244) versus 49.6% for a ~7B neural prover at the same budget — roughly half the prover’s rate from a floor it is almost never measured against.

  Stack Python · Lean 4 · Mathlib · PyTorch · best-first search

  Code & methodology on GitHub →

  • LLMs
  • Statistics
• 

  Agentic Research Advisor

  An autonomous agent that reproduces ML papers and is graded on the artifacts it leaves on disk, not on what it claims.

  Problem

  Autonomous coding agents will narrate success they never achieved, so running them unattended is a problem of accountability, not capability.

  Method

  A harness that treats on-disk artifacts as the only source of truth, scoring what each run actually produced rather than the agent’s self-report — so incomplete runs and honest negatives become first-class outcomes.

  Result

  A searchable reproduction dashboard; as of July 2026, 252 papers ingested and 47 reproduced with full / partial / minimal verdicts backed by per-paper figures and tests.

  Stack Python · LLM agents · pytest · static dashboard

  Code on GitHub →

  • LLMs
  • Engineering
• 

  Gaussian Geometry

  Turns three widely-taught covariance “facts” into exact, unit-tested statements.

  Problem

  Covariance is the most-taught, least-understood object in data science, and its geometry hides traps practitioners repeat.

  Method

  Closed-form derivations backed by unit tests and animation, in place of eyeball and Monte-Carlo intuition.

  Result

  Rotating a Gaussian and constructing its covariance are the same operation; principal-axis orientation becomes pure noise as the variances equalize; and the “one-sigma” ellipse holds only ~39% of the mass in 2D, not the 68% carried over from one dimension.

  Stack Python · NumPy · Plotly · unit-tested derivations

  Code on GitHub →

  • Statistics
• 

  Decision Boundary Atlas

  Makes SVM overfitting physically visible as the geometry of a decision boundary.

  Problem

  Overfitting is usually argued from the gap between two accuracy curves — hard to see, and easy to miss when validation labels are scarce.

  Method

  A single RBF-SVM kernel-width sweep in 2D PCA space, with the boundary first confirmed two independent ways as a consistency check.

  Result

  Added flexibility stretches and fragments the boundary into hundreds of isolated islands exactly as test accuracy turns over — boundary complexity as an early warning for memorization.

  Stack Python · scikit-learn · PCA · Matplotlib

  Code on GitHub →

  • Machine Learning
  • Statistics
• 

  Technical Interviewer

  An adaptive voice mock interview that trains you for the real thing — tailored to your target role and seniority, it asks role-planned questions, holds a real spoken back-and-forth, and does what real interviews never do: scores every answer and hands back a readiness report and study plan. Bilingual (EN/HE); runs fully offline with no API key.

  Problem

  Real technical interviews are scarce and give no feedback: an average corporate opening draws ~250 applicants, ~4–6 are interviewed and one is hired (Glassdoor), and ~94% of candidates who want post-interview feedback never get any. There’s nowhere realistic to rehearse a spoken, role-specific interview and learn from it.

  Method

  A voice-driven mock interviewer tailored to role (Data Scientist / Algorithm Researcher / AI Engineer) and seniority (Junior → Staff/Lead): it plans role-specific questions, listens with real-time barge-in in EN and HE, asks follow-ups and hints, and scores every answer on an 8-metric rubric into a readiness report and cross-session study plan. Production-hardened — every dependency degrades to a deterministic offline engine and the loop resists prompt injection — so it runs fully offline with no API key.

  Result

  A role- and seniority-tailored mock interview that gives the rubric feedback and study plan real interviews never do — resilient, prompt-injection-aware, fully offline, and deterministically testable (221 tests).

  Stack FastAPI · React · Gemini · FAISS + MiniLM RAG · pytest

  Code on GitHub →

  • Engineering
• 

  TripWise

  I built TripWise quickly with an AI-assisted (vibe-coding) workflow to plan an autumn trip to Italy with my girlfriend, and it reframes couples’ trip planning as a decision-integrity problem so the first opinion can’t anchor the second.

  Problem

  Shared decisions are distorted by anchoring: the first partner to voice a preference biases the other.

  Method

  Each partner rates options blind; both sets reveal only once everyone has rated everything — and the rule lives in a Postgres row-level-security policy and trigger, not the UI.

  Result

  No client or future frontend can peek early, because the integrity invariant is enforced in the database rather than the interface.

  Stack Next.js · TypeScript · Postgres (row-level security)

  Code on GitHub →

  • Engineering
• 

  Room Occupancy

  Shows how a random train/test split manufactures skill out of time on sensor data.

  Problem

  With sensor readings taken every ~30 seconds, a shuffled split drops a near-duplicate of almost every test row into training and inflates the score by tens of macro-F1 points.

  Method

  Compared the shuffled split against an honest chronological holdout — trained on the past, tested on a genuinely later window.

  Result

  Evaluated honestly the task is far harder and shaped by drift between sessions: a simple generative model (QDA, macro-F1 ~0.77) transfers, while tuned tree ensembles built on absolute thresholds do not.

  Stack Python · scikit-learn · QDA · signal processing

  Code → · Interactive dashboard → · Original paper (IEEE) → · LinkedIn post →

  • Statistics
  • Signal Processing

Research focus

My research is on machine learning for formal reasoning. I fine-tune LLMs to prove theorems in Lean 4 using GRPO, with the Lean verifier itself supplying the reward: a proof either checks or it doesn’t, so the model cannot be rewarded for sounding right. Training runs on a university GPU cluster against Mathlib-scale tactic data, measured against the goal-blind frequency baselines from Generated Formal Theorem Proofs that any learned policy has to beat at a shared search budget.

The same discipline runs through the rest of my work: chronological splits instead of shuffled ones, frequency-table baselines instead of only model-versus-model comparisons, artifact-scored reproductions instead of agent self-reports, and closed forms in place of Monte-Carlo intuition. It also shows up as system design — invariants placed where they cannot be bypassed. The goal throughout is evaluation you can trust and systems whose results hold up under scrutiny.