VINCE GONZALEZ

Formal methods · measurement

Punta Gorda, FL · contact on request

f-keys.com · github.com/vince-gonzalez · orcid.org/0009-0005-3640-014X

[Download this as a PDF](/cv/VG-Resume-Formal-Methods.pdf) · [all four](/cv/) · [writing samples](/writing/)

Profile

Formal verification, color science and epistemology. Built the tooling the measurements run on. Reports what the data does not support alongside what it does: a published limitation on an off-axis palette, a 58× gap between two plausible measures, and negative results published as negative results.

Published Research

58 deposited works · ORCID 0009-0005-3640-014X · all open access

• Where Formal Libraries Spend Their Axioms. Axiom use measured across six libraries and two proof systems by one program. Located an avoidable classical dependency in Lean's omega and computed a 13.1% ceiling on removable classical dependence in Mathlib.
• Which Constant Is Responsible?. Dominator analysis over 766,564 constants showing that reachability overstates responsibility by 58×, and that 60.1% of classically dependent theorems have no responsible constant at all.
• Why Tactic-Level Rates Cannot Attribute Classical Dependencies. A negative methodological result with known-negative calibration across four libraries.
• Eligibility Discriminates Among Theorems and Not Among the Constants They Rest On. Where the statement/proof measure stops working, and why.
• A Procedural Method for Generating Pseudoisochromatic Plates. DOI 10.5281/zenodo.21310578. Reported the tritan palette's ~53° off-axis deviation as a limitation rather than correcting it silently.
• Potica in America. Argues from community cookbooks, fraternal publications and bakery archives.
• Modulign / DAG-OR series. A dimensional address grammar for observable reality, including The Classification Deficit on Article 50 of the EU AI Act.

Independent Products

• OpticQuiz · opticquiz.com: Color-vision accessibility platform.
• gonzalgo · f-keys.com/gonzalgo: Axiom provenance for Lean 4 and Metamath.
• Trailer Load / LOCK IN · trailer-load.com: A trailer-loading simulator built because he had loaded the trailers.
• Also live: poticas.

Technical

• Languages: JavaScript (ES5–ES2022), Python, C#/.NET, SQL, GLSL, HTML, CSS
• Backend: Node.js, Supabase (PostgreSQL, RLS, auth, edge functions), REST APIs, JSON and CSV pipelines
• Infrastructure: Git/GitHub, GitHub Actions, GitHub Pages, Cloudflare (DNS, CDN, Pages, Workers, D1), Linux, Raspberry Pi, SSH
• AI & formal: Local LLM deployment (Ollama, Open WebUI), prompt and context engineering, evaluation pipelines, Lean 4 proof auditing
• Frontend: WCAG 2.1 AA, responsive design, progressive enhancement, WebGL, Canvas 2D, Manifest V3 extensions, VS Code extension API
• Docs & search: Technical SEO, Schema.org, SOP development, compliance documentation, DOI publication

Writing & Documentation

• Writing samples, with the source of each one linked: f-keys.com/writing.
• Shift reports, compliance documentation, incident logs and contractor correspondence carrying legal and regulatory weight.
• SOP development and a state-adopted request-documentation procedure.

Education

Ohio University. BA Pre-Law Philosophy, Minor in History, 2012. Gateway Scholarship Award.

Professional Experience

Federal Express Corporation · 2020–present

• Operations Supervisor, Columbus OH then Punta Gorda FL. Supervise a sort operation of up to 30 people against a fixed dispatch time; own the written compliance record.
• Promoted to Operations Supervisor in May 2023. New hire facilitator for the outbound sort.
• Hub Certification first in the history of COLO/432, FY25. Bravo Zulu 2025, Purple Promise of the Month 2024.

other versions: operations founder writing