SPB Git

spb/wp32_uqo

Public
2.0 KB · 14 lines latex
1% Section: Limitations2\section{Limitations}\label{sec:limitations}34\begin{itemize}5\item For $n>40$ the lower bound rests on one certified path (the boundary certificates plus Lemmas~\ref{lem:31}--\ref{lem:34}); the fort-cover second path exists only for $n\le 23$ and the exhaustive paths only for $n\le 27$ and $n\le 40$. For $n>154$ no certificate exists at all and the proof is Lemma~\ref{lem:32}, which we have proved but not formalized.6\item No Lean~4 formalization was attempted (toolchain unavailable in the execution environment), so no statement in this paper is formally verified in the proof-assistant sense; the machine-checked parts are the DRAT proofs and the exhaustive enumerations (Appendix~\ref{sec:scope}).7\item The DRAT proofs occupy $39.0$\,GB and are not shipped with the archive; their SHA-256 digests are recorded in the result records and they can be regenerated from the released generator (about $100$\,s per instance). Readers who want to verify the window without regenerating proofs must trust the digests.8\item The value $\Z(\PP{24r}{5})=12$ is cited second-hand; the primary statement and its hypotheses were not read.9\item The exhaustive oracle relies on the correctness of two C programs; they are cross-validated against each other, against an unreduced Python enumeration on two graphs, against the Burnside orbit counts, and against DRAT-certified refutations for $n\le 22$, but no formal proof of the programs exists.10\item The heuristic searches of Section~\ref{sec:robustness}(f) are evidence of absence only in the heuristic sense.11\item The search for the smallest working parameter $p$ was restricted to $p\le 24$ and $n\le 30$; we did not determine whether any $p$ certifies $n=25$.12\item The literature search covered Crossref, OpenAlex, arXiv and Semantic Scholar with verified identifiers for all $20$ sources; three sources were read in full, eight at abstract level and nine at metadata level. An unindexed thesis or report containing some of the small-$n$ values could have been missed.13\end{itemize}14
Files · 8fc58039993d24cfe77551af0fb7a26986d00767
Menu

Theme