M=13 Theorem
From Polymath Wiki
This page proves the final theorem for the m=13 case of FUNC. Assuming all the previous lemmas (which at this time have not all been proven), we know that if [math]\displaystyle{ \mathcal{A} }[/math] is not Frankl's, then the smallest nonempty set has size 6 (if it had a larger size, then the average set size would be more than 6.5, and it would be trivially Frankl's). We also know that no two of these size 6 sets intersect in 5 elements. Using this, we prove below that [math]\displaystyle{ \mathcal{A} }[/math] is Frankl's (as long as m=13).