| \documentclass[11pt]{article} |
| \usepackage{common} |
| \begin{document} |
| \notehead{0302}{Dependent type theory: the minimum for reading Mathlib statements}{Pi types, \texttt{Prop} versus \texttt{Type}, decidability, and ten miniF2F statements decoded binder by binder. Companion notebook: \texttt{notebooks/\allowbreak 0302-dependent-types.ipynb}.} |
|
|
| \begin{problem} |
| \question{What must we be able to read in a Lean statement to know what the reward actually measures?} |
| Note 0301 showed that the kernel certifies $v:T$ for the type $T$ \emph{as written}. Whether the reward measures what we want therefore |
| depends on reading $T$ correctly: which variables are bound, which symbols are hypotheses, what \texttt{/}, \texttt{-}, \texttt{$\uparrow$} and \texttt{$\forall n\le9$} really mean, |
| and whether Lean can \emph{evaluate} the statement or only prove it. This note gives the smallest dependent-type vocabulary needed to read a |
| statement such as those of miniF2F \cite{minif2f} and to see which hazards are in the statement and not in the proof. |
| \end{problem} |
| \stepcounter{section} |
|
|
| \section{Notation} |
| \begin{center}\small |
| \begin{tabular}{@{}lP{10.3cm}@{}}\toprule |
| Symbol & Meaning\\\midrule |
| $\Pi x{:}A.\,B(x)$ & dependent function type (Lean: \texttt{(x : A) $\to$ B x}, \texttt{$\forall$ x : A, B x})\\ |
| $A\to B$ & $\Pi x{:}A.\,B$ with $x\notin\FV(B)$ (non-dependent)\\ |
| $\Sort\,u$ & universe at level $u\in\{0,1,2,\dots\}$; $\Prop=\Sort\,0$, $\Type\,n=\Sort(n{+}1)$, $\Type=\Sort\,1$\\ |
| $\imax(u,v)$ & $0$ if $v=0$, else $\max(u,v)$\\ |
| $P:\Prop$ & a proposition; a term $h:P$ is a proof of it (0301)\\ |
| \texttt{Decidable}\,$P$ & a \emph{datum} (\texttt{isTrue h} or \texttt{isFalse h}) deciding $P:\Prop$; \texttt{decide}\,$P:\bool$\\ |
| $\uparrow$ & an inserted coercion (e.g.\ $\N\to\R$)\\ |
| $a\mathbin{-}b$ on $\N$ & truncated subtraction $\max(a-b,0)$; $a\mathbin{/}b$ on $\N$: floor; on $\Z$: Euclidean (\S3.4)\\\bottomrule |
| \end{tabular} |
| \end{center} |
|
|
| \section{Derivation} |
| \subsection{From $A\to B$ to $\Pi x{:}A.\,B(x)$} |
| In 0301 a proof of $A\to B$ is a function from proofs of $A$ to proofs of $B$. For $\forall x{:}X.\,P(x)$ the \emph{type} of the result depends on the argument: a proof of $P(3)$ and a proof of $P(4)$ |
| are proofs of different propositions. A function whose result type depends on its argument has type $\Pi x{:}X.\,P(x)$. Rules (with $\Gamma$ as in 0301): |
| \begin{gather*} |
| \frac{\Gamma\vdash A:\Sort\,u\quad\Gamma,x{:}A\vdash B:\Sort\,v}{\Gamma\vdash\Pi x{:}A.\,B:\Sort\,\imax(u,v)}\ (\Pi\text{F})\qquad |
| \frac{\Gamma,x{:}A\vdash t:B}{\Gamma\vdash\lambda x{:}A.\,t:\Pi x{:}A.\,B}\ (\Pi\text{I})\\[4pt] |
| \frac{\Gamma\vdash f:\Pi x{:}A.\,B\quad\Gamma\vdash a:A}{\Gamma\vdash f\,a:B[x{:=}a]}\ (\Pi\text{E}) |
| \end{gather*} |
| with $(\lambda x.t)\,a\rightsquigarrow t[x{:=}a]$. Setting $x\notin\FV(B)$ recovers 0301's rules, so $\to$ is a special case. This is precisely rule \texttt{t-all} of the formalised kernel (Lean4Lean \S2.2: $\Gamma\vdash(\forall x{:}\alpha.\beta):U_{\imax(\ell_1,\ell_2)}$) \cite{lean4lean}. |
|
|
| \subsection{Universes and why $\imax$ is the right rule} |
| Every type lives in a sort, and $\Sort\,u:\Sort(u{+}1)$ (Lean4Lean \S2.1: ``the type of \texttt{sort u} is \texttt{sort (succ u)}''). What should $\Pi x{:}A.\,B$ live in? Two constraints. |
| \begin{enumerate}[nosep] |
| \item \emph{Predicativity of data}: if $A:\Sort\,u$ and $B:\Sort\,v$ with $v>0$, the function type must be at least as large as both (a smaller universe would let a type contain a type that quantifies over it; this is the design constraint behind Girard's paradox, which we do not re-derive). The least choice is $\max(u,v)$. |
| \item \emph{Impredicativity of propositions}: for a statement $\forall x{:}A.\,P(x)$ with $P(x):\Prop$ we want the result to be a $\Prop$ \emph{even if $A$ is huge} (e.g.\ $A=\Prop$ itself: $\forall p{:}\Prop,\ p\to p$). Otherwise ``for all sets $S$, \dots'' would be a $\Type$, not a proposition, and could not be an argument of $\land$, $\to$ or a hypothesis. |
| \end{enumerate} |
| Combining the two gives exactly $\imax(u,v)=0$ if $v=0$ else $\max(u,v)$. Consistency of the impredicative bottom universe together with proof irrelevance is the classical Calculus-of-Constructions result \cite{mathlib20} \S2. |
|
|
| \emph{Worked checks (notebook cell 1; the kernel agrees on all ten).} |
| $\forall n{:}\N,\ n=n$: $u=1$ ($\N:\Type$), $v=0$, so $\imax=0$: a $\Prop$. |
| $(\alpha{:}\Type)\to\alpha\to\alpha$: $\Type:\Type\,1=\Sort\,2$ so $u=2$, $v=1$, so $\Sort\,2=\Type\,1$. |
| $\forall p{:}\Prop,\ p\to p$: $u=1$, $v=0$, so a $\Prop$ (impredicative). |
|
|
| \subsection{A theorem statement is a Pi telescope; hypotheses are non-dependent binders} |
| \[\texttt{theorem}\ c\ (x_1{:}A_1)\cdots(x_n{:}A_n)\ (h_1{:}H_1)\cdots(h_m{:}H_m)\ :\ G\] |
| \[\text{means}\qquad c:\ \Pi x_1{:}A_1\cdots\Pi x_n{:}A_n.\ H_1\to\cdots\to H_m\to G.\] |
| A proof is $\lambda x_1\dots x_n\,h_1\dots h_m.\,t$ with $t:G$; the tactic \texttt{intro} is $\Pi$I. |
| The $h_i$ are \emph{non-dependent} binders (their names are not free in later types) so \texttt{\#check} prints them as arrows, with names dropped: |
|
|
| \begin{lstlisting} |
| mathd_algebra_478 : ∀ (b h v : ℝ), 0 < b ∧ 0 < h ∧ 0 < v → v = 1 / 3 * (b * h) → b = 30 → h = 13 / 2 → v = 65 |
| \end{lstlisting} |
| Binder-predicate notation $\forall n\le 9,\ Q$ is sugar for $\forall n,\ n\le9\to Q$ (so it has \emph{two} binders: $n$ and an anonymous proof). The sort of the whole statement is $\imax$ of the pieces, hence $\Prop$ (the notebook's \texttt{\#sort\_of} reports \texttt{sort=Prop} for all ten). |
|
|
| \subsection{Elaboration: what the symbols mean} |
| The elaborator inserts information the surface text does not show. Four rules cover almost every surprise. |
| \paragraph{(a) Numerals and unification.} A literal \texttt{2} is \texttt{OfNat ?$\alpha$ 2}; $?\alpha$ is fixed by unification with the surrounding term, and defaults to $\N$ if nothing constrains it. In \texttt{v = 1/3 * (b * h)} with $v{:}\R$, the \texttt{1/3} is real, $=1/3$; had it been elaborated in $\N$ it would be $0$. \emph{Elaboration order matters}: \texttt{$\forall$ n < 40, Nat.Prime (n*n+n+41)} fails to find a \texttt{Decidable} instance (notebook; our diagnosis of the cause is that $n{:}?\alpha$ is still a metavariable when synthesis is attempted, the observed fact is the failure), while \texttt{$\forall$ n < (40:$\N$), \dots} succeeds. |
| \paragraph{(b) Coercions.} A $\uparrow$ is inserted when a term of type $A$ is used where $B$ is expected (\texttt{aime\_1983\_p1}: $x,y,z,w:\N$ but \texttt{Real.log} needs $\R$). $\uparrow(a-b)\ne\uparrow a-\uparrow b$ in general because $-$ is evaluated \emph{before} casting. |
| \paragraph{(c) Truncated subtraction on $\N$.} \texttt{Nat.sub} is defined by $n-0=n$, $n-(m{+}1)=\mathrm{pred}(n-m)$ with $\mathrm{pred}\,0=0$. Then $5-7=\mathrm{pred}(\mathrm{pred}(5-5))=\mathrm{pred}(\mathrm{pred}\,0)=0$. |
| \begin{lemma}\label{lem:tsub} For $a,b\in\N$: $(a-b)+b=\max(a,b)$.\end{lemma} |
| \emph{Proof.} If $b\le a$ write $a=d+b$; induction on $b$ gives $a-b=d$, so $(a-b)+b=a=\max(a,b)$. If $a<b$ then $a-b=0$ (induction on $b-a$), so $(a-b)+b=b=\max(a,b)$. $\square$\\ |
| Hence \texttt{$\forall$ a b : $\N$, a - b + b = a} is \emph{false} (take $a=0,b=1$) although it looks like arithmetic; it is true under the extra hypothesis $b\le a$. (Notebook \S3b: the identity checked on $[0,60]^2$, and \texttt{a - b + b = max a b} proved in Lean by \texttt{omega}.) |
| \paragraph{(d) Division.} On $\N$, \texttt{a / b} is floor division ($7/2=3$). On $\Z$ Lean uses Euclidean division: for $b\ne0$ the unique $(q,r)$ with $a=bq+r$, $0\le r<|b|$. Check: $7=(-2)(-3)+1$ gives $7/(-2)=-3$; $-7=2(-4)+1$ gives $-7/2=-4$ (both reproduced by \texttt{\#eval} in the notebook). Python's \texttt{//} floors, so $7\,/\!/(-2)=-4\ne-3$: a Python oracle must not be used for negative divisors without care. The Euclidean law and the totality conventions are checked by Lean on a grid in the notebook (1464 points with $b\neq0$: $b(a/b)+a\%b=a$, $0\le a\%b<|b|$, and Lean's $(a/b,a\%b)$ equal the unique $(q,r)$; $a/0=0$, $a\%0=a$ on $\Z$). On $\R$, \texttt{x / 0 = 0} (proved: \texttt{div\_zero}), a \emph{total} convention: \texttt{mathd\_algebra\_33} needs its hypothesis \texttt{x $\ne$ 0}: for $x=0$ we get $y=z=0$ and $z/x=0\ne7/25$. |
|
|
| \subsection{Decidability: statements Lean can evaluate} |
| \begin{definition}\texttt{class Decidable (p : Prop) : Type | isFalse (h : $\neg p$) | isTrue (h : p)}; $\texttt{decide}\ p:=\texttt{match inst with | isTrue \_ => true | isFalse \_ => false}$.\end{definition} |
| \begin{lemma}[\texttt{of\_decide\_eq\_true}]\label{lem:dec} $\texttt{decide}\ p=\texttt{true}\to p$.\end{lemma} |
| \emph{Proof.} Case on the instance. If \texttt{isTrue h}, then $p$ holds by $h$. If \texttt{isFalse h}, then $\texttt{decide}\,p=\texttt{false}$, and \texttt{false = true} is absurd (\texttt{Bool.noConfusion}). $\square$\\ |
| So \texttt{by decide} elaborates to \texttt{of\_decide\_eq\_true (Eq.refl true)}: the kernel checks $\texttt{decide}\,p\equiv\texttt{true}$ \emph{by evaluation} (notebook: \texttt{\#print two\_plus\_two}). Closure: $\wedge,\vee,\neg,\to$ preserve decidability (combine the two data); a \emph{bounded} quantifier $\forall n<N$ is decidable by induction on $N$ ($\forall n<0$ is true; $\forall n<N{+}1$ is $\forall n<N$ and $P(N)$); \texttt{Nat.decEq} compares numerals. |
| Not decidable by any total instance: $\forall n{:}\N,\,P(n)$ for arbitrary decidable $P$ (it would solve the halting problem for $P(n)=$ ``machine $M$ has not halted in $n$ steps''), and equality on $\R$ (a quotient of Cauchy sequences; the only available instance is classical, and \texttt{decide} reports \texttt{its Decidable instance reduced to Classical.choice} -- the exact message the notebook records). |
| Even decidable statements pick an \emph{algorithm}: \texttt{Nat.Prime} has two instances (\texttt{decidablePrime}, \texttt{decidablePrime1}). |
|
|
| \subsection{Ten miniF2F statements decoded} |
| Source: the 244 test statements this repository evaluates on (\texttt{p2\_runs/r1\_baseline/minif2f.jsonl}; Lean~4.9.0-rc1, Mathlib pin of 0301). Lean's own elaborated form is quoted (condensed); ``non-vacuous'' means the notebook exhibited a point satisfying all hypotheses (exact \texttt{Fraction}/big-integer arithmetic unless a float residual is given). |
| \begin{center}\small |
| \begin{longtable}{@{}P{2.7cm}P{6.4cm}P{5.9cm}@{}}\toprule |
| Statement & Lean telescope (condensed) & Reading, hazard, check\\\midrule\endhead |
| \texttt{mathd\_\-algebra\_\-478} & $\forall (b\,h\,v{:}\R),\ 0<b\wedge0<h\wedge0<v\to v=\tfrac13(bh)\to b=30\to h=\tfrac{13}2\to v=65$ & 3 variables + 4 hypotheses (7 binders). Numerals are real by unification. Witness $b=30,h=13/2\Rightarrow v=65$ exactly.\\ |
| \texttt{numbertheory\_\-4x3m7y3neq2003} & $\forall(x\,y{:}\Z),\ 4x^3-7y^3\neq2003$ & $\neq$ is $(\_=\_)\to\mathsf{False}$: a $\Pi$ into \texttt{False}. $\Z$ subtraction is genuine. Undecidable form ($\forall$ over $\Z$); proof is modular: cubes mod 7 $=\{0,1,6\}$, $4\cdot$ that $=\{0,3,4\}$, $2003\equiv1$. Verified; box $[-80,80]^2$ empty.\\ |
| \texttt{aime\_\-1983\_\-p1} & $\forall(x\,y\,z\,w{:}\N),\ 1<x\wedge1<y\wedge1<z\to0\le w\to\frac{\log\uparrow w}{\log\uparrow x}=24\to\cdots\to\frac{\log\uparrow w}{\log\uparrow z}=60$ & $\N$ variables cast into $\R$. \texttt{0 $\le$ w} is trivially true on $\N$ (a vacuous hypothesis inherited from ``positive''); \texttt{Real.log 0 = 0} so $w=0$ is excluded by the hypotheses only because $0/\log x=0\ne24$. Witness $w=2^{120}$, $x=2^5,y=2^3,z=2^2$: fp64 residual $0$; exact derivation $L/(L/12-L/24-L/40)=60$.\\ |
| \texttt{amc12\_\-2001\_\-p5} & $\prod_{x\in\mathrm{filter}(\lnot\mathrm{Even})(\mathrm{range}\,10000)}x=10000!/(2^{5000}\cdot5000!)$ & Closed $\N$ proposition: \emph{decidable}; \texttt{\#eval decide} gives \texttt{true}. $\N$ division is floor, but $10000!/(2^{5000}5000!)$ is exact (checked), so truncation is harmless here.\\ |
| \texttt{mathd\_\-numbertheory\_\-3} & $(\sum_{x\in\mathrm{range}\,10}(x+1)^2)\bmod10=5$ & Closed; \texttt{by decide} works (axioms \{\texttt{propext},\texttt{Quot.sound}\}); $385\bmod10=5$.\\ |
| \texttt{imo\_\-1969\_\-p2} & $\forall(m\,n{:}\R)(k{:}\N)(a{:}\N\to\R)(y{:}\R\to\R),\ 0<k\to(\forall x,\,y\,x=\sum_{i<k}\cos(a_i+x)/2^i)\to y\,m=0\to y\,n=0\to\exists t{:}\Z,\ m-n=\uparrow t\,\pi$ & A hypothesis can itself be a $\Pi$ (here it \emph{defines} $y$). $\exists$ is a $\Prop$: no computational content (witness cannot be extracted into \texttt{Type}). $y(x)=A\cos x-B\sin x$, zeros spaced $\pi$; $(A,B)\neq(0,0)$ because $|\sum_{i<k}e^{ia_i}2^{-i}|\ge1-\sum_{i=1}^{k-1}2^{-i}=2^{1-k}>0$ (a \emph{finite} sum: the infinite one equals $1$ and would give only $\ge0$). 200 random $(k,a)$: $|(A,B)|\ge2^{1-k}$ always; residual $3.7\times10^{-15}$.\\ |
| \texttt{mathd\_\-algebra\_\-209} & $\forall(\sigma{:}\R\simeq\R),\ \sigma.\mathrm{invFun}\,2=10\to\sigma.\mathrm{invFun}\,10=1\to\sigma.\mathrm{invFun}\,1=2\to\sigma.\mathrm{toFun}(\sigma.\mathrm{toFun}\,10)=1$ & \texttt{$\sigma$.2} is the structure field \texttt{invFun} (informal $\sigma^{-1}$). \texttt{Equiv} bundles two functions \emph{and} two proofs; proof irrelevance makes equal functions give equal \texttt{Equiv}. Permutation $\{10{\mapsto}2,1{\mapsto}10,2{\mapsto}1\}$ checked.\\ |
| \texttt{mathd\_\-numbertheory\_\-1124} & $\forall n\le9,\ 18\mid374\cdot10+n\to n=4$ & Binder-predicate sugar (binders: $n$, $n\le9$, hypothesis). \texttt{$\mid$} is $\exists c,\ \cdots=18c$ (decidable via \texttt{mod}); the statement is a bounded $\forall$, hence decidable; only $n=4$ works.\\ |
| \texttt{imo\_\-1983\_\-p6} & $\forall(a\,b\,c{:}\R),\ 0<a\wedge0<b\wedge0<c\to c<a+b\to b<a+c\to a<b+c\to0\le a^2b(a-b)+b^2c(b-c)+c^2a(c-a)$ & Triangle with sides $a,b,c$ (Ravi: $a=y{+}z,\dots$). Not decidable ($\R$). Min over $2\times10^5$ random triangles of $E/a^4$ is $6.6\times10^{-8}\ge0$; equality at $a=b=c$.\\ |
| \texttt{mathd\_\-algebra\_\-33} & $\forall(x\,y\,z{:}\R),\ x\neq0\to2x=5y\to7y=10z\to z/x=\tfrac7{25}$ & \texttt{x $\ne$ 0} is essential because $x/0=0$ in Lean. $x=1,y=2/5,z=7/25$ exact.\\\bottomrule |
| \end{longtable} |
| \end{center} |
|
|
| \section{Boxed result} |
| \begin{result} |
| \textbf{R1.} $A:\Sort\,u,\ B:\Sort\,v\Rightarrow\Pi x{:}A.B:\Sort\,\imax(u,v)$, $\imax(u,v)=\begin{cases}0&v=0\\\max(u,v)&v>0\end{cases}$; so every $\forall$-statement is a $\Prop$.\\ |
| \textbf{R2.} $\texttt{theorem}\,c\,(\vec x{:}\vec A)(\vec h{:}\vec H):G$ is the type $\Pi\vec x{:}\vec A.\,\vec H\to G$; hypotheses are non-dependent binders.\\ |
| \textbf{R3.} $\texttt{decide}\,p=\texttt{true}\Rightarrow p$ (Lemma~\ref{lem:dec}); bounded quantifiers decidable, $\forall n{:}\N$ and $=_\R$ not.\\ |
| \textbf{R4.} $(a-b)+b=\max(a,b)$ on $\N$; $\Z$-division is Euclidean ($a=bq+r$, $0\le r<|b|$); $x/0=0$ on $\R$. |
| \end{result} |
|
|
| \paragraph{Numerical verification (notebook 0302, all cells executed).} |
| \begin{center}\small\begin{tabular}{@{}P{7.4cm}P{2.8cm}P{4.4cm}@{}}\toprule |
| Identity & agreement & max abs error\\\midrule |
| R1: $\imax$ rule vs the kernel's sort of 10 Pi types & 10/10 & 0 (exact)\\ |
| R3: Python brute force vs Lean \texttt{decide} on 12 bounded statements & 12/12 & 0\\ |
| R4: Lean \texttt{\#eval} vs Python model of $\N$/$\Z$ on 8 expressions; Lean $7/(-2)=-3$ and $(-7)/2=-4$ vs floor & 8/8; Python \texttt{//} differs on $7/(-2)$ as predicted & 0\\ |
| Ten miniF2F statements: hypotheses satisfiable, conclusion verified & 10/10 & exact for 8; $0$ (aime, fp64), $3.7\times10^{-15}$ (imo\_1969\_p2), $E/a^4\ge6.6\times10^{-8}$ (imo\_1983\_p6)\\ |
| Kernel/Lean elaboration of all ten, sort $=\Prop$ & 10/10 & ---\\ |
| R4: \texttt{a - b + b = max a b} (Python on $61^2$ pairs; Lean proof); Euclidean law and $a/0=0$ on $\Z$ (1464-point grid, Lean); $x/0=0$ on $\R$ (Lean proof) & all & 0\\\bottomrule\end{tabular}\end{center} |
|
|
| \section{What breaks} |
| \begin{center}\small\begin{tabular}{@{}P{3.2cm}P{6.2cm}P{5.2cm}@{}}\toprule |
| Failure & Mechanism & Assumption violated\\\midrule |
| Wrong default type & \texttt{1/3} elaborated in $\N$ is $0$; a statement ``true'' for the wrong reason & the author's numeral type equals the elaborator's (check \texttt{pp.numericTypes})\\ |
| Truncated \texttt{-} / floor \texttt{/} & $\N$ arithmetic silently differs from $\Z$/$\R$ (Lemma~\ref{lem:tsub}) & informal ``$a-b$'' is real subtraction\\ |
| Total division $x/0=0$ & dropping \texttt{x $\ne$ 0} can make a false statement true or a true one false & the informal statement excludes division by 0\\ |
| Vacuous hypotheses & contradictory hypotheses make any conclusion provable (0305); $0\le w$ on $\N$ is harmless but shows how informal ``positive'' can degrade & hypotheses are satisfiable; check by witness\\ |
| \texttt{autoImplicit} & a typo \texttt{xx} becomes a fresh universally quantified variable: \texttt{@t\_typo : $\forall$ \{xx : $\N$\} (x : $\N$), x+1 > xx} (notebook); with it off, \texttt{unknown identifier} & every free identifier is intended; the benchmark audit recommends disabling \texttt{autoImplicit} \cite{faults26}\\ |
| Over-/under-statement & statements simplified, solution given away, or unprovable: miniF2F has formal/informal mismatches in over half of 488 problems and 16 unprovable statements \cite{minif2frev} & formal $\approx$ informal\\ |
| Using \texttt{decide} on large closed props & kernel evaluation is slow/exhausts recursion; statement with $\R$ has no instance & statement is small and over a decidable fragment\\\bottomrule\end{tabular}\end{center} |
|
|
| \nextnote{0303 specifies \emph{code}, not mathematics: pre/postconditions as Pi/implication types, verification conditions, loop invariants, and a verified linear search in Lean~4.} |
|
|
| \begin{small} |
| \begin{thebibliography}{99} |
| \bibitem{lean4lean} M.~Carneiro, \emph{Lean4Lean}, arXiv:2403.14064, \S2.1 (universe levels, \texttt{imax a b = if b = 0 then 0 else max a b}), \S2.2 (rule \texttt{t-all}). |
| \bibitem{mathlib20} The mathlib Community, \emph{The Lean Mathematical Library}, arXiv:1910.09336, \S2 (CIC; impredicative, proof-irrelevant \texttt{Prop}; universe hierarchy), \S4.2 (the \texttt{decidable} class; $\mathrm{decidable}\ p\simeq\Sigma b,\mathrm{reflect}\ b\ p$; classical instances via choice). Lean~3 text; the logic is shared. |
| \bibitem{minif2f} K.~Zheng, J.~M.~Han, S.~Polu, \emph{miniF2F: a cross-system benchmark for formal Olympiad-level mathematics}, arXiv:2109.00110 (488 problems, 244 valid / 244 test). \emph{Not fetched; only the problem count, confirmed in \cite{minif2frev}, is used.} |
| \bibitem{minif2frev} M.~Ospanov, F.~Farnia, R.~Yousefzadeh, \emph{miniF2F-Lean Revisited}, arXiv:2511.03108, \S2.1--2.2 (informal and formal statement errors); the ``Unprovable statements'' paragraph, inside \S2.2, reports 16 unprovable problems across the test and validation sets; abstract: formal/informal discrepancies for more than half of the problems. |
| \bibitem{faults26} P.~S.~Ammanamanchi, S.~Bhat, S.~Biderman, \emph{Faults in Our Formal Benchmarking}, arXiv:2606.29493: taxonomy of dataset defects; release standards (disable \texttt{autoImplicit}). |
| \bibitem{cc88} T.~Coquand, G.~Huet, ``The calculus of constructions'' (1988); J.-Y.~Girard (1972) for the paradox that forces the predicativity constraint. \emph{Not on arXiv; not fetched; cited for the named results; the $\imax$ rule is derived above from the two constraints and checked against the kernel.} |
| \end{thebibliography} |
| \end{small} |
| \end{document} |
|
|
