nasqretfineqs

Lean4 formalization with Artistotle of the arXiv paper 1906.11174

FinEqs

License: Apache 2.0 Blueprint: Paper Blueprint: Website Docs: Website

This repository hosts a formalization of the paper "Reducing the number of equations defining a subset of the -space over a finite field" by Stefan Barańczuk, arXiv:1906.11174. The formalization was performed with the software Aristotle by Harmonic.