From 3399900b0d2dea2e3ec790249dacab9f5331da98 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 10 Sep 2024 16:11:42 -0400 Subject: [PATCH] feat: slides (#12) * feat: start on slides * feat: more slides * minor * fix: wording * feat: pictures * fix: clause count * fix: colors * dash * slide tweaks * add another diagram for the 29 point configuration * shape * diagram for the lower bound algo * perturb x corrds * ccw goes the other way * fix: citation * feat: add conclusion * Wording and titles * tRaNsItIoNs * clearly * fig * add theorem statement * tweaks --------- Co-authored-by: Mario Carneiro --- ITP/Monokai Dark.tmTheme | 410 ++++++++++++++++++++++ ITP/main.bib | 66 +++- ITP/proof.png | Bin 0 -> 32305 bytes ITP/slides.typ | 739 +++++++++++++++++++++++++++++++++++++++ flake.lock | 12 +- flake.nix | 1 + 6 files changed, 1211 insertions(+), 17 deletions(-) create mode 100644 ITP/Monokai Dark.tmTheme create mode 100644 ITP/proof.png create mode 100644 ITP/slides.typ diff --git a/ITP/Monokai Dark.tmTheme b/ITP/Monokai Dark.tmTheme new file mode 100644 index 0000000..d8de214 --- /dev/null +++ b/ITP/Monokai Dark.tmTheme @@ -0,0 +1,410 @@ + + + + + name + Monokai Dark + settings + + + settings + + background + #0D0D0D + caret + #F8F8F0 + foreground + #F8F8F2 + invisibles + #3B3A32 + lineHighlight + #3D3D3D55 + selection + #A63A62 + + + + name + Comment + scope + comment + settings + + foreground + #8C8C8C + + + + name + String + scope + string + settings + + foreground + #FFEE99 + + + + name + Number + scope + constant.numeric + settings + + foreground + #FF80F4 + + + + name + Built-in constant + scope + constant.language + settings + + foreground + #FF80F4 + + + + name + User-defined constant + scope + constant.character, constant.other + settings + + foreground + #FF80F4 + + + + name + Variable + scope + variable + settings + + fontStyle + + + + + name + Keyword + scope + keyword + settings + + foreground + #F92672 + + + + name + Storage + scope + storage + settings + + fontStyle + + foreground + #F92672 + + + + name + Storage type + scope + storage.type + settings + + fontStyle + italic + foreground + #66D9EF + + + + name + Class name + scope + entity.name.class + settings + + fontStyle + underline + foreground + #A6E22E + + + + name + Inherited class + scope + entity.other.inherited-class + settings + + fontStyle + italic underline + foreground + #A6E22E + + + + name + Function name + scope + entity.name.function + settings + + fontStyle + + foreground + #A6E22E + + + + name + Function argument + scope + variable.parameter + settings + + fontStyle + italic + foreground + #FD971F + + + + name + Tag name + scope + entity.name.tag + settings + + fontStyle + + foreground + #F92672 + + + + name + Tag attribute + scope + entity.other.attribute-name + settings + + fontStyle + + foreground + #A6E22E + + + + name + Library function + scope + support.function + settings + + fontStyle + + foreground + #66D9EF + + + + name + Library constant + scope + support.constant + settings + + fontStyle + + foreground + #66D9EF + + + + name + Library class/type + scope + support.type, support.class + settings + + fontStyle + italic + foreground + #66D9EF + + + + name + Library variable + scope + support.other.variable + settings + + fontStyle + + + + + name + PHP Namespaces + scope + support.other.namespace, entity.name.type.namespace + settings + + foreground + #FFB2F9 + + + + name + PHP Namespace Alias + scope + support.other.namespace.use-as.php + settings + + foreground + #66D9EF + + + + name + PHP Namespace Keyword + scope + variable.language.namespace.php + settings + + foreground + #D66990 + + + + name + PHP Namespace Separator + scope + punctuation.separator.inheritance.php + settings + + foreground + #F92672 + + + + name + CSS Functions / Property Values + scope + support.function.misc.css, support.constant.property-value.css, support.constant.font-name.css + settings + + foreground + #FFEE99 + + + + name + Twig Tagbraces + scope + entity.other.tagbraces.twig + settings + + foreground + #A6E22E + + + + name + Twig Tag + scope + keyword.control.twig + settings + + foreground + #FD971F + + + + name + Twig Variable + scope + variable.other.twig + settings + + foreground + #FF80F4 + + + + name + Twig Variable Filter + scope + support.function.filter.variable.twig + settings + + foreground + #FFCCFB + + + + name + Twig Function + scope + entity.name.function.twig + settings + + foreground + #F92672 + + + + name + Twig Function Argument + scope + entity.other.argument.twig + settings + + foreground + #E5DB7E + + + + name + Invalid + scope + invalid + settings + + background + #F92672 + fontStyle + + foreground + #F8F8F0 + + + + name + Invalid deprecated + scope + invalid.deprecated + settings + + background + #FF80F4 + foreground + #F8F8F0 + + + + uuid + 233F0694-0B9C-43E3-A44A-ECECF7DF6C73 + + diff --git a/ITP/main.bib b/ITP/main.bib index 53681cd..d724e16 100644 --- a/ITP/main.bib +++ b/ITP/main.bib @@ -43,17 +43,6 @@ @article{60erdos_some_extremum_problems_elementary_geometry year={1960} } -@article{06szekeres_computer_solution_17_point_erdos_szekeres_problem, - title={Computer solution to the 17-point Erd{\H{o}}s-Szekeres problem}, - author={George Szekeres and Lindsay Peters}, - journal={The ANZIAM Journal}, - volume={48}, - number={2}, - pages={151--164}, - year={2006}, - publisher={Cambridge University Press} -} - @incollection{Crawford, author = {James Crawford and Matthew Ginsberg and Eugene Luks and Amitabha Roy}, title = {Symmetry-Breaking Predicates for Search Problems}, @@ -689,3 +678,58 @@ @InProceedings{cube_and_conquer abstract="Satisfiability (SAT) is considered as one of the most important core technologies in formal verification and related areas. Even though there is steady progress in improving practical SAT solving, there are limits on scalability of SAT solvers. We address this issue and present a new approach, called cube-and-conquer, targeted at reducing solving time on hard instances. This two-phase approach partitions a problem into many thousands (or millions) of cubes using lookahead techniques. Afterwards, a conflict-driven solver tackles the problem, using the cubes to guide the search. On several hard competition benchmarks, our hybrid approach outperforms both lookahead and conflict-driven solvers. Moreover, because cube-and-conquer is natural to parallelize, it is a competitive alternative for solving SAT problems in parallel.", isbn="978-3-642-34188-5" } + +@inproceedings{24heule_happy_ending_empty_hexagon_every_set_30_points, + author = {Marijn J. H. Heule and + Manfred Scheucher}, + editor = {Bernd Finkbeiner and + Laura Kov{\'{a}}cs}, + title = {Happy Ending: An Empty Hexagon in Every Set of 30 Points}, + booktitle = {Tools and Algorithms for the Construction and Analysis of Systems + - 30th International Conference, {TACAS} 2024, Held as Part of the + European Joint Conferences on Theory and Practice of Software, {ETAPS} + 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, + Part {I}}, + series = {Lecture Notes in Computer Science}, + volume = {14570}, + pages = {61--80}, + publisher = {Springer}, + year = {2024}, + url = {https://doi.org/10.1007/978-3-031-57246-3_5}, + doi = {10.1007/978-3-031-57246-3_5}, + timestamp = {Sat, 08 Jun 2024 13:13:56 +0200}, + biburl = {https://dblp.org/rec/conf/tacas/HeuleS24.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{03overmars_finding_sets_points_empty_convex_6_gons, + author = {Mark H. Overmars}, + title = {Finding Sets of Points without Empty Convex 6-Gons}, + journal = {Discret. Comput. Geom.}, + volume = {29}, + number = {1}, + pages = {153--158}, + year = {2003}, + url = {https://doi.org/10.1007/s00454-002-2829-x}, + doi = {10.1007/S00454-002-2829-X}, + timestamp = {Thu, 12 Mar 2020 17:21:09 +0100}, + biburl = {https://dblp.org/rec/journals/dcg/Overmars03.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{90dobkin_searching_empty_convex_polygons, + author = {David P. Dobkin and + Herbert Edelsbrunner and + Mark H. Overmars}, + title = {Searching for Empty Convex Polygons}, + journal = {Algorithmica}, + volume = {5}, + number = {4}, + pages = {561--571}, + year = {1990}, + url = {https://doi.org/10.1007/BF01840404}, + doi = {10.1007/BF01840404}, + timestamp = {Wed, 17 May 2017 14:25:12 +0200}, + biburl = {https://dblp.org/rec/journals/algorithmica/DobkinEO90.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} \ No newline at end of file diff --git a/ITP/proof.png b/ITP/proof.png new file mode 100644 index 0000000000000000000000000000000000000000..f0b9757b5cf3f48a503b9efc7cf80e3486377c3d GIT binary patch literal 32305 zcmZ^}1y~$Q(>A<|1$TFc;1b+D1Pku65ZqyL4=zE2ySrQP;O_200*gBYOTNuH@B4hu z^~?0t(>*<1E!8#MRd-F~M`bxQWMX6h0Dva{URn(RfNh874GozPyOoi@~WcYJFe-G@=m(1yGHpue!sXLh*?f$w>_W( zDj2?*I^$O$h_^6mW8*=_)8gYtDBWPWUdmyGOvZoyjL^lx$_J$6-(URPL<<~Qt90k8 z4!HlbTrfqje+dw$rc~ZJylkKnMFbcP;wZQPDaSnLkJ?O$!tksArjI8V0rOmlu49Cah!;K{1+Pd95JUk!nv0(%XNx3bICBkX&B&tG zE9RzO2P>~_zf%w6Y1?Q5Ri#CD#=nLL?6RCs{NX11)A7ktKHOL5dqox-QdHt3(ZQM4 z!2%|cR@gV~uh{tL^#}tLA--)Q1B^U|#JH7pa(7+=c4^#sX!WqUCj>C{q65H!s=65o zQ94b+??Hq$nBXvuR2g$RE6cjef;w((-a$s@00z9R7!Lk$Rb z#-%9y!B1%){Jj;02Q(rkuS1+cn3dvoxk*H1Tvps{V%cQ8pJ);%Osw6PqXqLO*7|0v+5)|#rQ<%-zQL1B@ZVLV;p`q#E;OamlFJ(g_JMlx`Xoa zg6BHi4qvbWk;ul_HP~hx)X8F+iXvX{H7? z!w#-Cb1uKmNO($rQ-;uPDn*2_m4!Jbx9JaWFva;$9@${fXEoW6zKmL8aT@ii&g5DNKc9wQ7)_Ok zruclm9a{c5rD&KAw;!2KSus5YxZ?{&W)H`jq6G%=n0?V9aaRlr*IveXJSM)zr;B62 zIY#`m;|Q4=<4WKAcrvqhDKneOoJQp%3wy6|r5MS0u-{cBKA!fhOH?Ce(U~0T9l7gMbk0d-ypMxN?Zx`e)}N3lFDT@GF4dBaI<>|1H0P zJJt8n5T*_5_V1W!FwFcEaz9{%12Hb&^iq-z1j2C;$>yRjx4|jCY3zmh2>0PTavg$3 z;1?5=6`*_YYaWmko}rh>3CjRsx!3TUcl&pgnKxTO(}P!VZ6{SvL>@8C{G86F33EIYf+OVkc|TOr5hp) z#Mx*rXek(ssl;dkO3G9x-kyJTLeAw%YRGCxo|A5qJ}U4nsZeJv&siX}L2v^$XX(j_ zD0RvC6&4kJD%dZ^K6Xat0Qwy{;U=L zI|@B&*3_05Eh!-xAMxirN$q;=ow7^KgK~|Eg-QceuksJ7Jlf{v%371!tm-0p-tx`b zUkWVphqU%8CN(QHgsR-ttBtd3L}f(`MD+d2pOo)zjyH*E(NNF=(7I*whw#6s6UQA9 zZhoCAxq+Y@=^vFI8D>Z;DJaESgjqx$I83@vin5}yGF0uBGjt5zvhLbS$efSuyr{G`VN3#&Kw6nUg z2&6owG^adNS!r!)%~w@a*XZI@r!S>1om8{0=kZSQ9`PpgrrN3M6X@rkd9TN+hNwCe zN*7khZ8oX5n63U?U0f4sT5iE;X0LOs3lLbd1MfnT3#Vg$AN)9t|5>-Vb58h$v)2rH z=-n5uGpoH3*D7!)ZwfE3$!TZ(7c*mlRY9aIUj9v&5}`N`qy3HDm&L(FnO(KRxjmbM zj8naz-bv-7F(z#0Ij%I{9@{5fg^urMHwQ(Q{d%5_$=%7*$%RDPhjn9dV%7!E>q{dU zmR%byO9}d!S8bEDOIz#tmOIv-6XMD-wklwyJ5!{s}-@Er)#NDgSK z=#l8EF>O zV(($M(%q}v=6Y3VVXzjl@cpwb2dxaF|%QND7)siSm@=_N;j~+8BPB> zpH_(^w!dDaHD_FeanpItbR()5m+5a3_Jlec(~{21ojT#0LJ|LGoy8a5QES|8ZxzKt zEUQ1G(Tk0X&)i{Lc-|}Yrv2c})OLMfJEd#y1w1-@F}x$e5W5}IJH{;IU%yhn8{0%{ zMA6Fd5qPnzeIqnxG1%z-beia<(2aK!&Hk1D>(^vo-7$Udon_9Rls|%XEN;5bE~!6B zv@o?Jv^I2(x?JSSy{-L^_B8jj7i%r5*oj%SVW))dzy*PO9nusRx8wm1y7 zv*R7%Ei?NuKWH3jvzB}J#Vh-eyYadhWt!~ z&ZpPtXzTDf@nLg?qM_#};6{8?;wD%#912MMjdP7*C%Jpqp6uxteZC|I_pROSgXWgxkjzP;B~5_`K}OPbIM%hN@VrjOP%ER35pXimu_zxIR7(92&9@u!}z6 zzn1^DTvVt`ee>t~v9j7x(s-G9v@&Q}VH?uD`g`ffULipGPq4@8g=i1^@4RQwu-w6L zWA3h)$g}V(%8|mO_DQYMwq*Av$p|?irYoJnV<`ZEIU@u4`^gz#1{;vqe?#O}u=~Qm z9l)P*lY#h|0$dr_n!Y-dI1l6Qv|A!pjzfvp`K zDF3z#GIewVi%?Vl?dU((zvDFbwEn+6Ik^7Mw4f7Y|NDlWlZ}J@KW#%vh5wccezf*9 zx6_rjwukZz+J~qBm+(K;|6ecuZ-@UysPkWhJn#OS^1t5vKPfd`&0VA%?V&w_MgQ+= z{SWbfzx*FUVfMch|1U=T%jJJcp==gK7H0p?l8GXZ6X7mESCQ0OT15kzLS^iqiw$~b zgvP%qGzxUBlRlI{(@1$~2@Ox+X|_ii{^H$mZQgC{ZA()!I&wsT^l1boOhJL{DJ!wk zX{2b6m?=vneTEfF1HrH1DCi5^DTeD!d`>&?r+lcGL`COl; zS~hIHLj&a=kJIH3iDu6$)4QjW+RCH((v#<-rRq##PScR%t*#Ei-@o>_f0Lh~>HJrq zHHO89&>J7#NBuhvPHU6xZal)_u0mi) zUKkol$&}y;%j9W}=Wb+$L7U5wKXZ%U|IX)cYFz|G0ne9l+o@L}{0*J&>g?Bf?|!Bl zSJaygS7=shdHKf6{T4K}4U4^RA^A)iW%2b7 zRwNGpJ$qj?oxDun>~&_ne`YgK1a#3Bd%2Xl8)L353q>Iqx?NZN#bxsFJqR|6M$(9l zYP`$mLF-{Vphxgw!&S5RLo(NnmK{m;KO_5hd~?!JUX;kotyuiapnU|^ay4I-w@35+YlHR3? z=>@Y1P;-45{vhH10MiC+BG;z z^3-dMx(cA3eq8lhC{wk$-XFDro>mz_WE>`e?LR)F+;+DBHszD(%T+`lrC%@mF@mN> zQ<=1Ds+2_^Ke>(4rCPar?2jbaOl1jR1#FkAGw8=K6@;CJ|F(iW07^Q`h8^xQ_GJ3kX~;u%vpCX-h6tzF854JaGNp`nvw_PYZ2kK%E)S=xIQw6p zgm67u%0gwqrT1YyDp4sI|TM zr0kf-7Qz^2)*Vmp_!VbZy%lnuAUGlQ3QnSrsQ}CB3 z7;|TeGgkc;t8i*>tBr5t7}&3X}X=RsAl^= zSy$xaUN$896YIS7x>oPWsnDv?DUZ586DtY&Ld+ZgTgcGuctb|BT=72EL0 zBR-#|zv3nh->$Jps}Z}waR|5XffG`yT2~|yj37t;KB^28VOTU0kqWG_g(~QbRWK~T z|9gLj=gt=8uvCrlOkUfOQjiW6bK3A-J|n8P!m>}~((i_Qfob$T|C6QaHHAsn+vCdG z3ij?_lAGXprDN#BQWcxog17bf8sz=d>#oULM#h;v%of^2%z_CW+RilOQ4or2t1FvF zZmwnChh!%2Sej1)stu<74>l(?ozmG`51kxsLhvhW1WvbqcSs^`3kU?ghvFk^$NK0d z7^}{mA-l*%z6Vp#f$oktaCCBdn|>;abW}UHEXDs%7t@+PSg}9j!$`n(<1_NgS#<^? zjdr!{U5K#$umOJv-?5gMYO_NYSzr2#ibTE8()*=>fIrXMf|lFXmTK=WGHh#92@Jsr zHnRnxIhkXhUxU?2yXriiY-_tp)><8F{U67TE0(JD2}r~y7FR+iGPS-AAt_gZz>>!( zG5kV!mu=c(XnRp^Z%)-TvtsD54m_tQ267$*#q24)gG7}U4W<7Vihxal{nwZ;2?|)5*Sw@pb-~QhL1xEC2U4aI+-h0Xf_Lm?{qz!Y8Ue|!UnR8C3c^6dD{XGcOOhcxX}yo{7q4) znW%G}hlr3kvz%U7bn3*v5OEK=vYX&Prm*TCTYg5Kl~_W!=(rE?*i2cp*=s@jZT$WR zgO~nw$Y^%4#bj1Kv|0&oG}R7#tRfC0?GW)&yBo9HhllfwRr`gq`o|S=^)euGF9?Sf zbN$m|#iGsd)YnXpo)uO=*UpC9SleMvDO!$Oa6jY`ru!qB8cdX%$RMZ_eS9 z#Hm;9O|ZKERkX3yhNNMP2BQ1%H|M=~4*de?WikP$=F>X+TZE1#%+#n{5(O}Z^tl8^ zo)Y0IGm*0)1~6$ACp8_)huWmVo*%m&4>FITLlA}e8jem@;m~!bC6acD{4L$E6TuVb zBY*JWx?|6x5i7lnFuer)H0sv(o&N9>^j@p)X&)GNf_zTvhnxHhnooM)P-w)7K3PR} zDa}qfieae0#`w@LLXT*JxPV&jo2m`>b^GHr+uFsgdN66O(HUFy1;~W+fn!=VeiYFa zf!vkU^;VZ2>EB-w^qX+HeZJ214}HoqybsDkACEx&3+=*1jbVrE7n0}tC)2S{$*puxdNypz zoSdjHR8rwqX3L$9apm*h`!+(ah5e{wGY#x3e+)Royz>~37!W+nYFs3;yjNA)zo=NO zG>>s@G>fjOuqjUDG;k34W-L`83_Xp#W1~K;@8I&fs_UAtN4`AmQT!=GxtAfbf3d_U>{%h83x=naCE>4(PU7WI7yvawKKsFLd~}gWz_M zZh3qsif@tX->>TWXG-S7FlC z`?l+EE-?fm_d;)ls8MBO2=lW)9(cs_NK=7^VPYrS<3xUfh3lqn1nzOSRl-8h!B>)d zUVSDzj<^vI#NX}cxjKP%UK0Gs$OC!KFf-}gmNvD2#*&%czHw&YjbdeeHuBn3{9H*}eg`3sda>;LPX5x)G+eQB&B+PRZehbx0op zhD_+nLU0baSEkqu+tXUPchk_t3Bu`A1vuJ_{qB<80bZf*Kr7&iFwSANM~;QlFQF={ z@Wo6m`K$6D&%eVqd+{M*)w2uP>;d}S?i>626Y~@2&?9uAn>v6&n1u~A!4Sz^-nxJ4 zel*8pmbUrSOk7@tz=~5~hXU?evfgcD1EBd^ZZq! zRw4u@5a30Z@RGreJ+VAidL6j__oSM+w<%rZbg;|14St* zU=r*0177wh*0!8sHs2pcK;h;Efy1mq*U`xDCYz;~$0s$2Y^UWpB0d#w$UVgymlLLl zmMq@_+lTb~Ci^U~&>^TQjpEB4KK77?R-?HqL#VM+uid#0mlUo3MGpqhK&OymHC_D3 zYowKBE**wB7m}Ln#f(Es7RWaBp#?p^;rQ!Y^(Jm0Sw|=jz>)Wk>=Jozk-mBG2+r;A zHq+Sshu&Hr(W|-A$sNhBVY?{TF_1XO|Qt7B+P7+g)TbPeOR+(Q4tu75Kxtc(b`M_IpB3 z+)-ynY!E$tKCYM+zL`jXu~#PJ%5kFq7!GiBU)i%Q0c={?CO3*i{w4`at*ehr64exo zlK8=Z4|%et_uHDz?h)^L`0bPEBifY70cY@2uPUw z_gm~w2lUs^A38c;@7LRT(J2RPhjHx059|O~yi_|a=DIlnzrF4rdj1#&^Och8JnP<2 zSO1A|9Kzj;am(S9t6_5s(YXjlj$y+~wMJ0|8Kj=bVb@IRjW^dqXPkCMWCV7?(D@`(2!@dJ<9*mTnN7=M%aneDfwSp|3a zT8zf;x>lzZYJl`XR)b|}3lMD=*CTzG_jA>bUI>%iqo2Y&5-vAI{ho@t`a|V&qL%kV zO<8^+RUHzK*3)=|drh*k_@0`r^aKQujls>o58YM7JWy#t&O>|y>gUJ0+7%4#q$Sko zYaXf3zvg@(ZPCfoHz>r1;4jP3_cVyNe(I8IN4%NE1$Is-VKPr~_)`m)-AAEWAC!Rg zX%yTK69Pid#NkkRdA)+5j5%qY|R_nT!*~RM!RD1YKuIEWU`+5>|tU)!#d)f-$ri}kQX=i&3qCF## zz43`o&Dp4YFS&ZbkmK2xIy(3ZhIAgN3^Fakxk3;Wxev5UV~Cm4cW9H*R##}PC`ZM- zjd+8Y{|ZTZ&ad|L@xRI3h6I>{K6~8T(*KzZiFSoJ20Ujf|9WUApyzr@5sm?$=&w!l z7f}Lp)R@k8W~jg7I?^moybZw6!N~NwnbVZt+FLDH6T-tZOOM!G?(>P2keEV8QKLtG z9i<-j3|VzUj+LWEc50{P(hCtlW1vSx2jw{Qey7xkKCZysMf5Sym0hlOeimdwlZI{o z8OL6GmV!U2Z&j*h{MKE)(BexSTkg!w4?7jyLR;ck?!+=2_Z25>hCnoGD<=dq%2b|S zdW)%{Eq6h{`-^XfIX>VtE8Tf{mWSs#1@@y2Lz|s%q0W#^Ov8bv z-uGed$jfm3go$x9&opN0z?y!{{(Wq$=MC5Cqq7d`>{Q+$9;;||&&gOy6NXdK){oWc zAFcXMowcyu;)kp@i}NAR6sr-0(R2Rr1jW=DA06ff)aatD5Yc#2A#x5_^}!Am9lc~f z8ZpHY26)PtBw-?;crh!!)UmwuCyn;hq4j8Nd06-GqN5a0MJNJTyphmJp71UV1@Bnx z!$-|YuMIdwuVA<$xgW1cvF7?+;Q@-$X_cwnrhd~fn}x)MDj;{FI6@`m-Xuk7;EgRc z85_&ziA8`zU)e_A=jhp9gKRoYE-$hYojj5f-m|tW;s^w=^R>s(oUWMV*T&;){_E8blm=af5cvj|K0BYf^!+&53}t*gjJi*^ibXWbw;m{wha9`xz}AaRVJ@k zaJ;B+m?D)zD^;Lncy9|=CBBkB?n!Pjk(PhMa~bg?-HB-e1Cpp6{t&V)RPLHa-x+i? zvj231CzW+c*1{(MRpRdgFQ04twrwb}h#6VMQ>~CBZ4h^QorlDZ0hppE$CWU9ra*9 zW+zTUxkRvNqK3`9Ntr>3p-cPtedUrcna&2|Hxb2HkV>__R6NXQg;z8WNUyL@7rDCt;Iu2}sDGTs6D)Db(M6gN#F3!h$1AoSie-}ij$_R>` zAlp;3{(x$ubEjMSlb`LM*Fa3M@#i3i41=Phu0qFWr!Jyo>jG@ zR`!VzZi@YRoL>9p9!A|*j8wmmTh#Z9rTl?z3%$9gm6(y4*aX|}nOpFyq)sh2+FUtS+GY^!8=I1Z-Mo6_!{QR8wzgUYCCt)~m=6hZu{4bVHZJYNF){xK;c{Tkp>^R719aA@t#4G00 zSSdcl;)9C0kr3<5WT$8&E88nEWyn(1MP0Sg^HBMQ1ciW$&>6s7ZRb;z>6ss_?a~YrnLy_^tIL0-d5f5FQha%% zeibA36&cCaJsQ5<;mfB3TNE&N<2G0RB6I+f?5n&fGH95^gZ?dXBKK()Mw^0+DB`IQ z?Y@S;aM+26Pd}oj`^jvl1#=bD)H-?11$M}evCPmJIIT5V3mT&zq`U}p0xg&^3n?EG z(EDjXgob6F6=BVe+oEUpqd$#IqVU;`463M`+DeIeY|6N&h1In|+!w262UdY~c=zZu zz60qby#ta^08|VL|9=(W+qbdS1+?#{#Iq%gil<`I_m!sEu2gNY#>nv&SqitK*^hMAMsBvcrF<5Puhu{Kslu|_R? zdbS{V;c@*Zsf;o}Qx3`u&Ay?MSsxGYh&Db#cy9pO&xZ%xl zY!Bg+t-5Rb1RuQj`(njRo3A`$S9^nfqO~S`Y zVMVc~qgu%0d_nvHimJ_5vAOb3quWzrWVq9gAvm`Vb}CzQGTpb*wq*6bnJK%-Up0((C{ zO>j>`l-eh!buhisC_H}vd3=94-M9~tvCe3=lLG(=HbDz--phgh2qUWjmYmzag+3;p z!IJx4N{}J#{T7Z{)@U9Ai5uZ6E4J1h38QR^JZu!koloPu3L?(1vM_3JTlklXdIo$& z?~f{0;x`I6;?>AryV1}rwz+jib+q8mZzz?O~L#97;;BE`Qk%~30C4B!}nyzNl3XPH{7!J>+Op#EHm{FL|uz` zsmA$wt=5JUoE(nl!bjl`i@x;|_vZq7#=RFsUj`+(oxTsMl^qCc&etzHrirI!ATAgO zEjZ!x-P$I3iD{8wgb&|Li`C{py%AllWdbVlvAEcO6_)0p*hV(H-YvS?t4M~Nh}AY( zhrbI^b?9!{0Wg-9Q=@!~4~kQt@)&1rh1}0*OZ@zc`M2frBg`pb1Hrw_A;+IVvazJ) z!`v5FooP`+r|IKsBrU;3P!C?P?WyvTUk;sRM(M2B^5odq9O2$yobn8@gY`h~0D{n7 z^&DvMw?+*GJ%n%h3s{kG27b^?XJ?e-S#C$b898#DHfqn!H1MkiF|S=28bc?ZL9J9c z`XK#FVh&%ogXi=mDVy_PT+6ciLi8rLuB4C_tSg~P?q z9rfK7wy;B@fK0#JG@(wH?DX{&zPLj?Gep?H!yK!uPp72>NRZt+7>-{511Rn$?ss#* z%2{6E|LWaf>7#vR#HY>>Az`PZN*({rqxHKq6yMWm1hloGfW^+&nx99OcR}ErqBE4x zNm$5K4)-%=ush{1;&FFE>Gzxg9>*KH&6sh%KbZ!XFKEz`#iF9_k^1XoSq&&PCyRF> zFwWq81?R*>L`4UJa;{BW3xivoQf0&B&6Y1P5ne#F>+hmOeo-=rD znPQ`JDr)Qod$|{M)|R>reKZdT+6QBnJ6XNvQWZXJu*64%t=d#qp*>48$i4)g=k$r# z{EWi0399R@lV~gG(b2UgOx)2nq>EkTT|1`|3_RpyV33p3zGOMa_zvNbYoE1OF?#<1YkMED`+N`8R?ERm_3MiKPE*mjSLb6@>h_>kjEN*lESiPFIMIw0{k%{lFz_qCTm7qv+H3;IWj49~6_VO<-p*Y1WcozDmnE#z68I_W z87VKZIb~OU+0Y|3W2e4{0r?1fG)WuH~?AL_%r4}Qy|@s^{7O9;Rh5tLjK}1)V8Xe)3usGoqM`FD&rKjqZ zlk+rU&rg4jdrW-6&ME}lhFtvR2(2^pz;UlDL?L*o$3MR>{wySG8y)!y?F3}ncub2v zR~adKp51@sW;@c)5`9tf#A*+u8o{mqM^>j-p~g%J5fDI+l9xLlFB9iQblJ!K#*84$ zBlR|BwotBe*~mu;Ryqfs{esJk+-cmvGM4|gtSHVo*(wqai~?ukFSMu6V{uE^3|@Wk z?*9EY?4$9TQH`&_YgH;cgAewY+VThS*FYd_vuma7B=PXZ*0d=H8Na8v{Yssx5 z`jMQD5zQ6A5b)e_(Or2kkzII?*x`1`P)^T=;P!FH2vW#`WY}G2EVihfX81ij7qG_J zITZ8wzB(aZP}2N$C~#X~;`wJ=%S5_t+^T)!Vqg%g20Li1a*=I#DZ34MM6$D08%xt!}WoB?VeMFkf9$hgI!bQ;+YZ?w9PRH0w zZh!-4-!ryH%LJIiLrf1<2NFeWBMl_vluN(Bw+~9Cg1`!_GlOX$7=)1@WPN$g1hL2{ zkVF!A+o3x|R=9UWKL{^q2~I9XBVqP;kJ8^+Cl(|&-B3liiw3ggPy$pN;4W}?TIq*z z@4vR-q&WA&6Ii7PTj^gqT!z=>!MTKM7* zQ-aNEBu=n&7LJyf#4HX^&t>VaY*l3fbrCQ8=#{!{-$#Y#d5}+If2?Y2kex{Oa=yYI zwN1vFke+2BnzpON66RYrSSKBAHH)?IJ7c68^q)9a9v#kR zL7iblS~qNU=z8>G98RJ&_PG4fThSVmd`ylG3vRKRl?2|o^3Y6Y;W0B4H|2K~q4f`z zBd;6gn}*VeF+)|4Apmb53n++S)Oqk4&n8ZIy*`2jlGriqN$m#+7G`%m;Z)W+e5@Bh zoIGEsPqIK5eFir?Ob~&7LK^)0xv+yIMSw1D!Tiz%ob4+lEBF&KS-Aq7`0)n|;m;S+ zu!c3^Nr)X00(hlxW}hMaYHHL1Z(j&E@v!N>KceQF*a>f`d^OoKW5;fZ#^fCE!89yS z;UIzEsu7F$2 z+ulP1*d3}Lt}DUs`yL*%^>edQIb{*wnZ*bvNFy)5!QA0Ikl^)>a#unD7g{qu=4PTz zLA_0yWZnaCXBI!L@%FekUBKnIUnJy2SrD-HI3lE274xERBG+IS^uBWxq8+rM&t)C~ zz#d5A&j%fji^F|oti~+{2c6VJu)R{gG@F+1@;c<_^y#C`Fd2Hif#J{hC^+YU;(8cE zdrArm7bJbw4Rue5k?AMI><73;ebobq1$MjdZ?D73Mmmu)hc2nGsvDnjxOTBu@W&_n z9)!DGzx%c&%N44L1EYR~_CVpaZu4;qd+wM&o}Ig^u`(Ot(Ep@fE37U=)8`K$S&s%p zI1~2%b5*+PZV6Mvze5ARdN3S>JQ?B>k-Gs(BDAswASZoYM6Q%f-;Q<{b0N3-I|5kE9^ zBdFbZ0Xo6r{8SKvfJ&IxuQ{JjXxR|Rrs^Zjh}HZC@@3E+y&&LJ<)BesmEd_viR(9y4xC0FQJ-pTK4jj7M!F_CB#k8VjEJ2|mZXZCPZi1R*2BE;`# z{+znl{l|~sc7d}d3&B!G5pMENj1^C9F>9J}cbWVAfl%B7`YYF3G%AhM%DYq4o$>k) zOhIf2u(Ny$_^ev42a}77F1n5zFf)}5s4^s+#K+`DJ=f9?nKo0>B>2dU(evi1As83QqQ50b5i6Ig@SWV6IKDpm%g2IX z4d)SD+<-LFc(|uq#bmh9-Ea|$!KVN>(FN+ORQ4D1!Jlx5l}2H~YY9-`lq27{Wo^_O zs{xSF5g%(Lqa~fFf`k546Y&%aM*;1GLmcevUAKuj z`yBUP>}62ASVMjEIS0O-4#jYYa8TlMN#D^roc!jS4?4zNH1x9$>9CQjtm0wTW+5<} z%$yvC-PA>-+$xjC@_>`sQ_>kjx{#nXCqsOFsjV8|_H}FmU znv!}fsgV0A$keKL9xeMG4fGv!4tdPz!Q>*|6(Fhb3VdDN!6oa! z6}dt&H3hgbpCG#>kEQ!0<*}v5zWrnGP>wwo_C$N{r~yJ@Mp^6M_r5%L%<@!E;6&5s zTn<`QaRQo*mJ7TY@%0D%Gfj1<2Us@Xot_XUb@L_$yUXNHVfnG-ogK*ANJ zyvk3tCmL5X^Q3qG10(OrSAD2;#koRc8TO^mYS^EecE0n_E}UY9t|Fuizu<#YOZtrQ zjed^t3QroVoizJ%d^-ilCx01Lbs#uhy?%70u{2S1KQ0NC>wy3lGGwzS@y#SamZ=2J zGbEWWR7NRtqP_`exWrHTjz86z%M2Fg+RGw?$F{`YO`L8Im6s38G{|AJDMKyqWcgDd ze(~&87Qe3Q?&heW`7V+W?e|(%iS6N}_ix>GRM`R2Y;W6??@pGNy>LA1Xo$i$C?2!w zzK&v}uKdN7FUppAbOSHj6O-186;jhGI5ThR(|!bPo~tJ$A+POYW-v_zVs)!*C8vIG zNyv=G3Hg{V?LD^wmno@7I8q-4-(GLSaXr?adX z_$`M_%?i7DbTn@t~&okKT7?B0%* z^>IIun|GxJNoYpboM^qK7?*rNOGP7J^(n_KRUjima>c)P!(iTG973!_DyRo_jZ)D0 zA|Vv6?f%l<~(f$Yl+Gnoy=%pL+DK1e9+ zK5?8olp(`E?CCUC6aYi~Vk1)D(*yZfu|8jY3Ob(^W}icZlx8}#%kx;xP+~Eu{1V{C zg3MXuz@t)1rd&Pw5QX`VDbUWqE2;(t3wvdGPY_H*L*eUyri333>QMDb(}B~9vr43TU;gHSd2VI}P`)O5$R;4#BD*~X$XW3yj7u+4|pWj}+e9w9W2S!o} z9X(@0A6siavAUlcb>Mtx48Mf_l?SeYC=R8Bz>oxKR#UH|^cvhI7f}06A6F`a_m795 zHf=_k_zG4QI!BzwO86#N0eZYssANASpYJu>E|VRb5uWoG$;F*>;j^ip(RQ|`;Cl7) zyC1WY1+gW!0-Zt{9q|r^t#*qa?vh~Qy9RbtYmNMXZFnN-28A_q=wQ%+Q>VH> zPShj-k)e!5K|Gb1bH#mOu{UQoH}@-k-uSOD4&X+Ee|>lzw|RUUmWjeUirJDFywbBA z)Vy(Gm3(bd!7Ae>VCI4f%M5ExdI-=ESLsePO-z_hLkac6;WKAD2fSUR#2wqz$^<`QqNE&m#%jte>tIXedP!1`s6K2LTijv39phb1*TK0X!_ zqfN5Oo4U*8S*^Q|q#JJifE|c8O_QT&35MSzh7Gh#800kSjV}?TnT`V8?1@-5ZCg^$ zgc9)}5Ro6~gvxXk#jxGrp|W`$v;3-KpK_M{b9K7q|9rM46+0iZ5kRULLfcMO&x86czFoHYru2pXXV^rJUF+*kpZdK0 z@%xUt-2ME!d4bjg;r%o<9?vkqzVB$W+qg5=!$;EMIDU?kXtN00#wuc^ZCQFq}Q6)Kw?-Nf%E&efVEMob!kVT?~2~Sd{$0Ux^#exmK2YKUAO}Eu* zz8gW+7&dptAMif#9KjsuptA|vc?7We{VzA!^<+Aze-iz9GN*KwHYt#eh4F-b(3DEW z39}YMWj&i3`Amq^ zB~}rZy~|egqmixvOB%?FYO;FMrq#Jk z^)~xMfO@I&qP{HvAsfUV=+{RC2qnA>5s!a!@&;U~Sy_T6bB+-f5^zKv;uIej#8+Nq zZ}u5z;z`7{!O*4?gV%_76?o$ZNKYjU#6?)S7VPo*D`|p*3Ew?$nLdWpG&DBeagU}b z-!g#eJehRiI^moY81p*_5e`iyt92VK>M=!YUE#dq{26>B%EG0ESQUL(X1=h>r8<42 zR$Wm8S|U$3+z7DQiW9I4<=MpTt9$?K&vBB3w@1{hQIlWlE)30`_!Uh6Neuo!y`5!H zTtWBdad&rj8Qg*mZo%DyCuneoL4&)y1PJanXmFQ6u;3mv2?2ud<$eFPwOh5HxB6?s z^u67E`rJOh=jl#v@8pIeD+UE2{qv;fUzXCHW+fq@qOOK_iEFLK_ReE@u5nSYdYxJ} zaD=$`+0XR^l4-|FQGIZ2c&wS>X(!Xug0 z0DFaPDj32&1C(ySKp?SELSS$6ww#8DgwIVk}H-5sS zl?nlQktR^slZJ@&t3vR&{XV5L(V6W!lXV%yI%h-6nDX^Z&Ue)& z^8*wA)Pvw#(6B3t%g!Co!;wh+;LzJ++8Xjb+#+;(WS_5D%4OWoLnkYDniwreD%?KwJ zlIMpt`i0-GR+W`ZT#{;isi+j=i%#+h0jWi<4isq-aOn42GJIg%sq(ooZh2pqkokpH zviSW1Ad30>xT9OSk~n`YTDbh66J^GJS0ai?ut#9lX;}vP)vi~C;2)8k>yCg3J$&FE zu9>wuxO@Ie9~!l*(wB7dWv~o_aUZQPfCMe)6eeR<&HD0udr01k*t!lD0+`O3BYJ{I z2iKu`L(a}lUcI<9M)~FS<|`B#bndV6?kQYMYjM{E4G{XwS&PwzohU)eAjNV9QHAyv zUTFEOVi$e=$_Hu-;^Y`aK9z7X4wi738{AV)FTxvfYZ%(86_0mhj&HI|&MF&jCk4(0 zMvK79vf&bszXspr&p!4tD3p-(v)60{rMFs%aQTgp!hi@15VV{A}WrL7!jd=Mczt?aD^KT`bA8C+j~b_0)sPPIlX^INR)U2!??f5 zOU1*>1Bv3Lnc`1>O$Vgl8-}~kN#MDKiNU4V=pNV~2C$C@GGIQ|zv?u8428-^kqjrZ zgoZJ1WG`6%%}D^ayB#R6ZFg!&ue_O{Fl*Lx${&2cMsdiK4Q`K-eY;37n19q~(pk!p z@emYaEkU!@R@4Bd6#F>$)ELh0{|Q8WHH_l2KQ)Pq%!UNmaS+tRs@Yrj?;co_StIB`*`>)&;VzoorWMMhliJS<-Oc6?Rb=9U z?vH1{6j21DvSrdX)?A; zE^8VgYcTy&i(iXeB@FcN1QKva(dPP5Pn*B60v{+1XGtJsiC$G@`;&a?9_{dm{Vkme zubzggMtsOLVyE#Hg&`9wV@c%DaNn?FETZ&;_a~-pqIuuCUtKnEFwk4h_M3Yi8>;-7 z0slDClX@Nk+WT1j_XW_`F>)<+t>U(sHu{G?e(tT)s-O4(?XK?0TuRm_IZ+)mh z|4Ho3${7bzyOwC8m#Y|TC01njx$N=Qty^K3(YQGgs5-Tu&wn$1J9}JOZKsbns>W|| zp}0(8dPwFKL&Jtl9(RY0YzqL)D0?d5xEyu4ckxH-jn7MP8wLVIcMrhn=0je-XjI$a zxReL7Rn$?`BC?}|oj8U;AU9?W>*;%520}2ghPn}XWk!&Ir)B4@&YI5)HVn+m%bf6q zC=85%<*O+3Jl{Ky@cZg0b=e?@GJ^@kVmhJ4S!58k(oj@VZctL5H6&Xat@L;qPi7U% znqwI~l0eu%8-pwN?x!5WhnT;cx&I`#WM4LEjf zGA1S1vEg*RNPz^{%yP+;=1wAUCb=|dRU{x^FJxK@v=;^AYEbF zc=H;wR^?5L0^WROj*C%M4LeA@oNZ6!w#AY8uJj4#O(E9kO7F1LY0Gu_$_v%pp zUk_U^i@h$x;4B5mE?>YT#;CRGW9&wk*J)PfM7TH8*h#Ac+v5zesIJ*Ntn<}o{S;h) zu6Uz2Bl!YHD(2I`ueHfgGMy`!>-p>HrI%|m1N7a~zq+4Y@_U`Ov6|kqSNqYTAlIFDO68&#o8go9y|wZ6N>v8F&RB3e5(#^p@J?xkkp32`Dd@i_6Q~N$~b1 zU2%S|FVI_hb4Z9KZhBJGn63w&lRT=EVmS(_$rE4WM(40h8GpkWnLHtRhm-)&cV;8cOm{ ze4Dfk1KlKv8%^=UR&S4{HLS-j9vG9R1=tHMoZh*^ek^WyRY}KDi16N&Q{EOt&ooQp z<-P#YB&UAR>{*2g9Q3(&b=GmHhLwdn8$Kv>8AXQ0WJdH->}B@D69uA&FY^jIfb>{{ z(FYuWc(Snesc3{^4s%zz`|{-YVYNig{inxSquW3<^8}!SEpuIniAl*9^_m#E-Ap|q z{ENtn*Fi3AlPl;1h!pP!$ZS6RXgg=qsmpL;iSN6Y|KJ#WxyVWdoRv&qY#ueTksz_+ zIQoA_JYGAJ()0lmy-GT--0sIelY|gw?4{*cg^8k&u+P1r>m6y6;AIJT*W{BmJjQ?7fx69sj|GEN<+R`_Y+s?-$SgajlJqRGe9k*|-LiDW= zE;>Cj`FF%p6bqiO*5|sL@$RLsDDbOl0VL}5Ru>TGe;pA|F|AZ8Lejy2YR$8oOr;hE zQJn$f6! zC{}~TtWw0vr(cTJ@s_nG3l-`koLyMQ<-Bgu^_3WNa)uaVPn);B6+jU)JCNNFUV676 z;>FTNERF=A(Veq_x5}0e&b&o&5WFM=lW)f&;|U|l$Pv&A75C4S$Jsp`zrHy_YRS8O z{7wL5iJw$V5=5vb$w_>bM9HO(Cx2+tJCdzqX_G`@9v&V(EPR@wnlFJnc{0*53F$!k z`1P{VS>i@wlb+0uBd!HoV*)`A*7P1BX)tF333Wx**dTq#GQ8`>eO8>={cwsWmsd}# z&YhQ$57$d~V;?NJTez4FDU*Sj=JBfnMYI_$lPH9pojm4R}y!Y(4LFiwQ+&@ID;Guy7aDO+Zm~DN7`gE z_;P!(@UadO#kb@KUIo&UIQ`K-2kaA_j{0`7&a1KyThuTcfKG25SzmPVScgo0uy=CIWZ_^`fNhHSP;KEKR*5T`F~)@VOzSm}|}Z zvTH>!H=K`NOB-|zBiOQ$%>=`;jTEm*Vv!8n@q1RC1FL0c%Vci*Dgb4FsI|_ZaUl4^ zMB%CjjB!h1IVU~=qQ}n#O$ACDACHU9qZ}SY3OzG%=MAGn`!KkO2xd}g z|4|a$%ke`9J56Y7nNA4ENE$&M!iP>LX1~bd+MVBHu1ir3KX)KLNEYw52k=ztjW0T(0x+t|@YZQ$bvqK3B z31%a*O7R`_<4M1Mm5(sN;H4+5WF7?cfT72H!~J}NH(`9ke^Xr4Kylgmh}m#JiEy0a z5{ZKYBgZrbyYbge1ml>l8CNTeklGNf6w@KQY>@KU2%YQqE(se-Iy~P$R5?Lq%{b3} z?XlOjd-&hATM7ZySunuTNYE^Vr(>RD{2ok{eC}|iMn8oI6W_*P2HkcMs>y7ZV@l2; zLd<**(&4B-Mq~O(vGEgKp%bwP((PgcNyFu6ca>WO@ETdzx98h+I%JAu!24w`gh@kX zZatOIYFvVgjy)`kLAj3yqzyTHc=1}1KC>N-x4O%di$-;Ta5B?#J^J}?g=7R1olGU9 z9p#c!nfcJ7X(EvYWVO+}WJ5r2kg4f-H*V;G?aIJL3S|DV999u!J88wt)i_={q@sH; zugvin!06F#B%am{_&yrkH|5GcO6^ws-rLfgP1N6?$ z=x(5YJm)NdIE%KzU{i_7`rV#XMyH{DkF99qclx%-0&l-mg(4=%N;3rLltZR7PlApr z0$`wRvoK8`w96-QU3xxnbU6t8MZLWc2FDv5+uA3O+T>Xq7yxSh*utUI#)Z6=f<+2-u zIG2d>ya0Gxd?VbfFa}$8%=Gmw>qN<Si9h^Z7Ef9PS-t zIV-){_j`mq6)pR!J#}Ul2=}SEv`z=SbHj`=9cl=+dsJmhZQM;<_^aVh2oOd+g5qTr z6rpa2L2kzqo60%9OO$b{6z^<_xPLnA5p#_GMxXp3JLW4mGt#n zyLxoe6Db$0Gjv?Da$f@1Aou`6R`&^HE#(afmE3g#?|^FdJ1tg~_DaGPW`pAJK!8#jbD^Jt{Eh zc&@l|i+fuc*#kanfFU~9lhm8uglx-a57UZ}0kK1JDb;vi%eNS!0J`fW{d*V`l; zDjq%qxW#-iaZGi}yd`Leza7T$9F#kai`6b?NjP;Azt;OXekn};k#zW8#Trj8$jj*V@gTP8xCDV*>>mUE0Im+*xaf^0c-bEmyhj@5upXU* zm?QFCgLBku()k(=x+NxlDcUrojOb`S3LL#swOh! zXtd6G8I^q2RP)8^7#2r-4!L%g@~GWMoWwFN33n0glG{v(+9n}#rak%`FK%jOqR;8(DBGHa(4<# zdTE*IH_9a_99=)7L}KBfQ^9zNn&!C0xV7%kjjDkHNvt{G06UU@DXZHOQH_x?kTA(1 zPID>%6=j@S?OwydFNn=wEZSM)Jti5qhTj)Yq6P<6d~kd8VbJ>@b+t@G?8&L>B8D-s zu~zZdZ))R3JWu#JHTh;2G1~*nd+=1pzSX-(9%%2?z?p)LRS+*tJygYihwn}E;Z@j= z!*0mreFO`MAtPLJx_*MtxW&EujhQkJ?C&m1#a0q{Dbb6*#I3Cp;tlNdBK{PUeWG@J{+Oea1XhJ!&`uaPZET^|hh*pXm zhksQXw>!IK*alv%c4dxlzKvr#Eic?27W9;Q@%T-5FyCeC?6d)`J!>h^ljD7y+93-Q zFliQPS4N-P=y7QO`A}onOz7B6TUbQ{^`0#bEIAvY4Q|n<3C@TN!w|K~g7URUz#xA>9&V=c7w=m|`8m>&*oPiAA%sKH`JHNcLaR(0z;=)HSCf3Ui0 z{##7CGpq*ppbm4a=W0gOX0zKjq#*n|>G7^FYT`Cw6KW?#2@7=yXyV-x+z1)F1nMas z?iJN6Om~3>5&)WgH;kQb4U~N@6Qd6toeODUd+5)S7-yw_ApvZI-O#(UOohr ziY=A;S%M)N2Eit$AOYQz9pTzkbE>-bF(xu9fs-vRvGMk$Q_6SQ?Cl&{tU`c|J& z3J0aC*f7-BJXVx|T!j|Yq?!GT57Wbyv9x8D_nM4O^vwa2k9k-nP1j%2LkgdCr3qi!g z=A)^UL}qo(*@g(FIsrvkjg1hHKP{XeHRTl+nf}V>4_1i&(Gg$4hbNh5rgw+XxH;8n zZEH45&t$^KM(FdAcwPu75_zA;C&E$MM}^>ke$FOdHi$t*45^@q0`I01R_#})n@rmH zSM;hXcDogS<~L1;^fIXkXhkZPtwl+Un}&Grd0v#P$5u+L>o9;1D>oJ#Vlm4h6m6IM zTWlC3Qn;}&^37#8Pl%bMW^JT(Jwp^a{2viS51ufqN}5I(9%4v#(Wh!PaHh3{HTv@o zcJMLvp#Amg$i)s30*{EVEm4X!ivCAS7}m-^rPNPjLtRYnfi| z+Q><}HepS9^l(m&iYaZRYjdq-j+a?yjRi5PYND*-vIkxP+ zpM26$vC``DzATOzb1%zWYH|7kXOR#6RI^os2&oeHzs>T}oZ5XBR_O8R?q}1D1@Tm* z@mkcLt#`({`eVUWu!Ko!PF^@zjj;6RKJ`gd%IRF8{zJ8)Su(Kq7g~mPdtMtFtFtOA~gA!PgDnkZ#Z4I2qgA z$C2`?_23h6J=d6^@&#|<2j0MMTpO)LX%si^jbt~8Mb}L-0EAW)ueyxRIHX~{NGec7 z>#G49zu_cf&&>&mA=I(baX#nkn4*`N{}1+`#&nrxZk2zR8tW>E9(5`K9B+WnffTj) z8Gs(hutSS(aV}E8dA`y>HF_RDcF zUSzC4MJW~({dA1aXmX7Iz)dr%&JZbE{w^Pdeu-_DT{DVSGJe5(Q045yFBBC}@TU+Y ze^Uv#4PnE~?8~!DgN|{=uf6KWS|Hp@6khI2j7u!4)NYj^ODE909#e~{Sq^_dSN`iSg-k7;)il!z0hl63v^=zzZTeIDZX2OX2y^?tO$ z!%vgmOh7;%`hp&_TRAUhq0Ud*haKv*cbvIRWM(74-s^VvU8IC2c)b)-`Q`4Wk zSc|!+T?}@rf`iQ#gvAKc-Tn~l;otKccSPW(6kAd&_Jo(7WbaRxbn2pJ^Y>g?9^E2z z8tYBZi*=>@jK2aocO^@;Y+`?x&8ZjHs&WbcaV$K-He08Rpr&$gDRRqqeC6FxG0jri z4gZeael2jq%I9QMIh7|Ov+->)rCK^tzhN6H5$NYYjb#7Uk@&*`G@exxKRpiZ`8Nio zs0Trs+>ltR2x*8zG&EsQa_Ndug`mZ0gKiUAPe{f8mG}<$CTL5GJXxx(j*h>qRK|Bf zI!8z(`gcv%3gucB(KmWy$`mL(9;b`5^#}GCZ!Kc#QyFHg#Dm{lH?ZpHj;-=#m$m~f zH}lI$`x{N@{C|MF*aT0}eK%h_+4t;9rr?%{(gT z9rB@3A7Wk%yG9`x80h$_!!GM2HM(`*-h05B9*Ug8ToDfQJivnvrB0>SAfT}vVrr+5 zTX};+s=&XRrLJf(;;k59MOhVuiBWMld1E?T^g|e`kA;Y>ubxPJAVf2%uLUlNDA_}} z7`obGTrBvhUL+bW4>ymFRHc?4*u=5Uf}=F~w-W1s90z7^bGVB|HFV`zRP!;GmwTCTS$1&^Hl4Rq!-R7U5hmiMm!S7)h`kQdiN ziSceB+dleS!=wi10R>)-RZ>S~^cx<;`=&<3R$^AGpBy3Rtg~asVighmj@Gy&1^~?b zj6*J_z_jJS8KK|v>In2LMGfOWWDOq`&M%O9Q&I19_`4f17#B%IXvdu9?xA8jyzNX* zZN|91YR%senCDf8(gdR8g7QmiDXHRsVm*m}Z+`dO>bz5)(mxD%fqfDP@{>hu|NEx( zR55G-uCn&B70W9El$7pQVY|FpkCs}0EqORVei9w2aoBqJz%_LJfN_mRS_0=mPbds) zd3`Fxy_%HT`s+`ey5w~WTF4~4Z$T_L(-Y2cmQ9n1t;ql1&Zp^anWeX~Q~JA3O52K$ zoJ$7#N^2#N9g?SRC0_pudQM-D@C>_lBsXox@@vdDpT4$PSms}w!I;)4utc#no2_|; zC7fxWsigToo|?bd*St6D{1J@#4sn%?2EI|DvCTa^N&kJKM)<4Xx%}kQ9qrc_7%3g4 zuhO=tt2u%@0xxG|%AA(>QDwqWUzXLj41{Qdw?gYGPcC;2JTxD7Iz0h-9Z8(#_rR*R z58Zrxi}aD+Q8A!*t=wWr5(7DtB%{%TmD^Ej3N9g@sPwZI%9(LmB+RfS<-TXCq#I z*+F8l3Uj8F6XD6PYw2zi41Sm(D~Kw*!|;H$Rb7Phh;uF*|4v-fA}`JDOR za>a6$Ye)MnlafH?GxDg!4%vaWT`nijb#|& zUE+Od#zviv5)*6vn%>Ya8*198YeY3rp(m$kWoErhceV_e zXX0&3JB9sc9PbCcwD|#_l^RIM$qw=st7uJGaeq_@C%H%Zbq{1K&Nc2oaaI%)EUd;? zFrJ2t;xh7l2jpeDag^M6Rn3-d{4dXcv`wZ}YVUI*{+#kW*}B;3Q*Yhvk|FH4xi6w8 zv$-i!J8_GH#4)xvSQM}RxOs1Kg4RmW!?#0u2S!ZAJPoU*l{#O$jA|c>@L2?EPOba7 z6v!w;))qm(hv#|CZ_n#JpD%T7W~c%)p4e)_QK#CRUK-0YjH|RO>NF$sf<}J2O^jD4 zHXjlqMpI6VD%r0FK3%(_{maOWLEXIXdiGkl>rAhcGjIn=yKL@9Q-mm5$#7i!G4A4O8;vUAOf0JBoEy z!Z9c{{%4*Hb2V%-Xs1GGtD^$XzX9t(e&@={?)tyifW?~7Df_u*)l~>Gm11WJ(gXYh z*#jc)n=hApK-^T zwkMd{|BxOxfi1@wc`)DMl$mD9^Xf|Qjd1+2rWjJ5FwhsQ4bm~s`V@ybE1CMr>~BCDnWmsnfv{*mkEKu) ztBdc82O06p9)nWbNyz07-eZDknTUn4VtP(BLjuhl8 zIJt!1maB?Izek@Ge!y|CDo34UcpQE}(Kk0n3=djaG3ipbSe+S>NJmrGIN6Jrsg#md z@{z!Z%Ki*wUiWb+k*+0acvmDM%#ND}{Bx?eG%$JNQwka4rx__1{zFcQQpH%@=k6U#9NmwfWR?y(0w%AoU`RfDD!9u-B&_nrQX&P@Nc6tdl;Scb&}^|3hJeuccccD& zN{_zf;@B+ZwXzx|BPLra+A(V8$4AIwKBdbRStZCy3{pWQ7rsjBwLp~eQDFwYI$LgE z3-+BtJ8Y{ZG)1SE=#9+`<#b*iA<#Z8BWB0213!)q>tD5H3g0Qd9F6cWsa%0up?({h zt_!k12kv2KNh*XvT^&zLIt~=Br5!&?gjqE8^~JK@c>g>L4tFcGJ9)O6Xsj&r?lR*3 zm4((!@V!6OxVo*ATH0BZFiUd|lhmzgs8JZNR3-E?Pkk?w`4?js9Ll+)kpshAA-#OE zU!37s_Jtya-tBFFV9_0tLJu8UN1BN)wPOP)dL!4hN+1_!+0FcQ4}{s(F|p@tX~nWA zd(|&yar6P@L_C-DFWmwePe;gs2~Edq4u01sti;u~CVfFqsvHeZ5*IxAU}6yz70e>k z>eS%cm>;E^5gNruf( z5bc@lna;y3m??Y~z;MGxaNlj!?SL~oB8n3(IZ%*%OI5&a`+S|z_CB@kF5Wxxku%)I z6tHI;c@nQV@93j#e*$nKp+@M~W{`A!V5=iy}@ka6=%e34mbarqMQw*R5{= z!GMlCi2?~`Oc+;^jG0KtFo9<&{B48MAD8X^5T*={RWB`(Eh8^iO_|>VeljK*j4;A= zVpB2*u~o;$z@a~+;X9gi^zS?Yhqfu5$%`D6NoRId?nV7nISbty!|HN=%~OfGGXqHX zc*)1hVIwh@XR*>+vzGU+o!!JKv{O zB}`isQ+1|!*Pa1?c;pM2n}U`^#7vBQPu&#-sc*#{25Xex%_3f8P@T^@r4%6OkY_$l z!WO58wjyl|>;|#LYGZX3>}vtnCWZ%PS?j?OPM4z@O8E~_bj8kKbC|riAI$c;H;4F2 zi_R;znqcpIwt1pT&nPXeg~fPM2QS{D+G1#v_oeHYmb0b0fLfNTTI3(xV>)Eqipe(- z-$qAHn6B3I96~@lE(SlNt}u5cd5ItRm%2JaB~aHiri#-BMU!r`1bW#}XC-So({4)Y zr?xu!*MD%Kdl&}4$4+EggMa)C*zg@puSl-QkT&Z`@e!G<4M-=54f$nrTIPd6VENG; zH4xoqUjQ9VZ*xyj`(M zB>g%OR9Ht(B#!5}9&k0yBrjxo&a{9PiaS8RN$1>Uxt1Z8Xemr-iPuy(uG;q(E$RpvlD|7%(#0>G`ihulV z)xlx|IAMt_3Z+{r$JJjl#U#Jh$k%cKFrBgPQ#*C7VnZzqyznI~Ae$INS5US)FwYux zOoqE|v>M5wphX#Hem~G22^%>0Js@;MB9Zz4f4QW0#)qV{gV?mgGFZ4*f z3+QQuTv*5VB3eBX#*-i;-u|LO9IU8mo3B#}Ds_PcComp{S&b;PI=BzX&XzSw@4gz? zu|MaiLK>wTerLddH7ru;$och>s)|lfJYccJh#xkQ;=M6T52tgpefUh;2f)crR)C|+ z$Vso|u-j@UyPtY(=>>FX-QufLjq8_6oD9=~2;n+-bIP|XviOLm24PXd@$hT-f&_oy z!NI*yEqVj5^KZJT#sa#rhP!w+x%?MCzjx*2pM{lc!7QJ`@K(>(iy7+{E!D(#^6zK# zBLPI1bEC^s=wi)cNvvkNFbFzlEwNF5G3iuNz@?C%v zg`m~xhrE=tOYKVlORO_HAzB!ogWPo|Ko>7Db(d%%dKhFykq?LBGo5}VwtV{KgUToD z;|mGRX{Dfj<9ODy{Q1NTc(*4k1x;Tq>Jgr0zsF2s{BL?=g?Nok9I^5u zO__3@pr+a!(WMIrXEuZu+c4iVxiwcD596z!F=dp9>;?THff@EVjtc*h02A7`;x zQ^25~BOcd@sEisKfzMBdT#fi%diRIuAPd#Q8xKiW`#^7aV2*L)B*DX(mdu5kp+dseh#tuu;SJd;e} zl=zwCJ#d|CKkSAHd2-b$HfZzxOCtedXS)%5OuHamk1M$SWMrr{z~>{3!ycVya^cH3 z9Br{a31!UH5`%$p`=k`&SP)&vimUz4p^16zjf}>(Bft57wOdJw7CDIQBqYEmz~7C* zB70cHku71Kh-kiGng`XNB1t?Aalv@iE~Q<;LjPrGzY`s^K~e$zMq9-7+80i$ra*y% zqDXw+sF*PUEzeKu79865MYYp9Cm3Z~yWikDyABN|t>O$9Fyi^fQHihZyS)qii?1xc zq{N%}V}<8MB>Nu)^Qjxt{m#XX@b*#v(zLO4-biil=ij|)k;>5?rX#bK{g7u~<-J({ z_uVFM)@K3A-~<1<+-rA527vC;Bf*`H00?880C6lx54&Ej-D)%eX+MP_Ecm@z^bdxG zEm>8pFs?3Qk{>@r{_~`rQ?QbAjHQ&>{@JJ2zZrw*IY<>jlDVhGzE}+C9!iji3Umj` z7e~PSfN+?4JoRi%F+fj)$J;+hmzr{})*h?tM*9H#2IAc1<%HRB{?ylDvU|X0HQqYA z3(zUyqHlmv-KT#YRT6=wzzxr3Q|UtmyxxCS%PR;`(WF(Y7h_Q6cY>>9V{Qt*_%C-i zURcLQY8_S}_kL^-rEg$c_om;;ka6nVg2~z4d!m^T>kv?e$qBB+{c$PNJT4me((h9> zpABmk7sTWc?bN0X;Ak9OH#dZ0;D5qE!}xdBS!#vnbyHn|`v;hvE_2|anx#iU-V`4x z#%!>Ji^zH25YYDlmJb+nm=pIlT+GJgL?HezL!Gd3VH}+(!3JMHdY0cTC^6?-=YCWe z4awVs@w8(t=YzJ(|VgE}o->lYkQm-k+~GPZa&o9m~oAxq*dD^E}R9*MW5y zJl3)NM{&>`BW}8?yZZgPY!L}KE+XvS1ts<-C(5~_kP^9R0G7kUhu5GCQySZyC_+uJ z*4@xTUZ96HWBuW>&-^r`*U{45urG8>^v1xhahsP*c*|kDb@|QzOz<5FpgNo!aH{JT=MPxdO>OCcZrGs>=#nldg;yE^*iGH!ye61V~U+8#E z_c@?HcRxFfy7s%$kiT{y^b~kd?y;vc;celhWs3d>1brKm3~Ik)S^!ki50^f##4BJM z{Dhqe+z2qk0ICLrXhtc!pVz4U^WmWx_!n6Y6kjmr7&#z*ou+TRGwu_a5DVj^$FWrnOq(-rWDmX(d+$;Pkp@7O%4sUBUY?#Y0mnJtYCVp(+T*YOp54Gr zl)Z!Vr#2ltKYmbb24^@)BSbo{q^aQ4p!(lxzvNAkvvg1iZKB!oXcMCONrGE z*RZ!FFA3d(UU80V9jq<6EYnF__h=nL0}B) z+<=f7l}u}U?#a0?0T8d*BJSmmYb~tYzhnAHmFxeWtu73e7uz^3l*eO`3%+ge`pidP z^3r?J{NMl2MnR+J{rK;W`dK&8;!Bv}5Qy{~M;2;RZm;@rwTbwnbG|le?qgPzFRC>A*uB8Qrq~wL2=v=M5e{L)+@&qCj?wfM{|5_Ur_6a!Oo5wDSb0U(nFd@(_iv2G>RYvttaya&#NFIVPX8eMI(ce5Yg?IOrr| zp5|*_V-Bhos-0k!=$aA6GQiqaYIHaPtu|V9QOr3WODz_e1+u<3_+n<6hEugBMqQiR zmRxE?fb2OKcmynCU?CH~&UdcJanEo6Szf?nQ&Jc-*(W=$_tH|Tb_!A;S8*ce5DI2m zt$Eb7%^p!r0sn6M*ER$m`e{_StHJ{qy4UuP8d=ZzpNXE6$q@Ur_1eBi!~5S}&hP6u*qqLAHrW+2ZM&6ys#^F3wNna( z2YPMX)yr=`XJ8}OOd!}CUaWK!hybDd|J6SC16#HByPU3}|9L&HG3ftn|G&Bs@`9Z28m#5aj_`VI PBaD)qnrxl)yU_myM6>UD literal 0 HcmV?d00001 diff --git a/ITP/slides.typ b/ITP/slides.typ new file mode 100644 index 0000000..edb900b --- /dev/null +++ b/ITP/slides.typ @@ -0,0 +1,739 @@ +#import "@preview/touying:0.5.2": * +#import "@preview/cetz:0.2.2" +#import themes.metropolis: * + +// Like cetz.draw.grid, but allows independently specifying +// where the grid lines should be placed (`from`, `to`), +// and how far they should extend (`froml`, `tol`). +#let grid2(from, to, froml, tol, step: 1, ..style) = { + import cetz.draw: line + let (fx, fy) = from + let (tx, ty) = to + let (flx, fly) = froml + let (tlx, tly) = tol + assert(fx <= tx) + assert(fy <= ty) + assert(flx <= tlx) + assert(fly <= tly) + assert(flx <= fx) + assert(tx <= tlx) + assert(fly <= fy) + assert(ty <= tly) + let eps = 0.000000000001 + let x = fx + while x <= tx + eps { + line((x, fly), (x, tly), ..style) + x += step + } + + let y = fy + while y <= ty + eps { + line((flx, y), (tlx, y), ..style) + y += step + } +} + +#let lean = "Lean" +#let thin = h(3em/18) + +// Many slides adapted from https://www.cs.cmu.edu/~mheule/talks/6hole-TACAS.pdf + +#let config = ( + aspect-ratio: "16-9", + // config-common(handout: true), + ..config-info( + title: [Formal Verification of the Empty Hexagon Number], + author: [ + Bernardo Subercaseaux¹, Wojciech Nawrocki¹, James Gallicchio¹,\ + Cayden Codel¹, #underline[Mario Carneiro]#h(0em)¹, Marijn J. H. Heule¹ + ], + date: [ + _Interactive Theorem Proving_ | September 9th, 2024\ + Tbilisi, Georgia + ], + institution: [¹ Carnegie Mellon University, USA] + ), + ..config-colors( + primary: rgb("#fb912b"), + primary-light: rgb("#d6c6b7"), + secondary: rgb("#fafafa"), + neutral-lightest: rgb("#13272b"), + neutral-dark: rgb("#fafafa"), + neutral-darkest: rgb("#fafafa"), + ) +) +#show: metropolis-theme.with(config) +#set text(size: 23pt) +#set raw(theme: "Monokai Dark.tmTheme") + +#title-slide() + +// WN: I think this should be first slide, not the 9-pt example; +// it is really confusing to look at a pointset +// without knowing what kind of structure one is looking for. + +== Empty $k$-gons + +Fix a set $S$ of points on the plane, _no three collinear_. +A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior. + +#align(center, components.side-by-side( + cetz.canvas(length: 33%, { + import cetz.draw: * + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05)) + on-layer(1, { + circle((angle: 0deg, radius: 1), name: "a") + circle((angle: 72deg, radius: 1), name: "b") + circle((angle: 144deg, radius: 1), name: "c") + circle((angle: 216deg, radius: 1), name: "d") + circle((angle: 290deg, radius: 1), name: "e") + circle((angle: 30deg, radius: 1.5)) + circle((angle: 240deg, radius: 1.5)) + }) + line("a", "b", "c", "d", "e", "a", fill: config.colors.primary.transparentize(20%), stroke: config.colors.primary) + content((0, -1.5), "5-hole ✔") + content((0, -2.0), "convex 5-gon ✔") + }), + cetz.canvas(length: 33%, { + import cetz.draw: * + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05)) + on-layer(1, { + circle((angle: 1deg, radius: 1), name: "a") + circle((angle: 120deg, radius: 1), name: "b") + circle((angle: 180deg, radius: 0.2), name: "c") + circle((angle: 240deg, radius: 1), name: "d") + circle((angle: 200deg, radius: 1.2)) + }) + line("a", "b", "c", "d", "a", fill: config.colors.primary-light.transparentize(20%), stroke: config.colors.primary-light) + content((0, -1.5), "4-hole ✘") + content((0, -2.0), "convex 4-gon ✘") + }), + cetz.canvas(length: 33%, { + import cetz.draw: * + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05)) + on-layer(1, { + circle((angle: 359deg, radius: 1), name: "a") + circle((angle: 120deg, radius: 1), name: "b") + circle((angle: 240deg, radius: 1), name: "c") + circle((angle: 30deg, radius: 0.2)) + }) + line("a", "b", "c", "a", fill: config.colors.primary-light.transparentize(20%), stroke: config.colors.primary-light) + content((0, -1.5), "3-hole ✘") + content((0, -2.0), "convex 3-gon ✔") + }), +)) + +// TOOO: speaker note: our points are never collinear + +== 5 points must contain a 4-hole + +#slide(repeat: 10, self => [ + #let (uncover,) = utils.methods(self) + + *Theorem* (Klein 1932). // WN: I don't think a citation exists for this + Every set of 5 points in the plane contains a 4-hole. #pause + + _Proof._ By cases on the size of the convex hull. + + #components.side-by-side( + uncover("3-", align(center, cetz.canvas(length: 33%, { + import cetz.draw: * + + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05), + line: (stroke: config.colors.neutral-darkest)) + on-layer(1, { + circle((angle: 0deg, radius: 1), name: "a") + circle((angle: 72deg, radius: 1), name: "b") + circle((angle: 144deg, radius: 1), name: "c") + circle((angle: 216deg, radius: 1), name: "d") + circle((angle: 290deg, radius: 1), name: "e") + }) + line("a", "b", "c", "d", "e", "a") + if 4 <= self.subslide { + line("a", "b", "c", "d", "a", fill: config.colors.primary.transparentize(20%)) + } + }))), + uncover("5-", align(center, cetz.canvas(length: 33%, { + import cetz.draw: * + + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05), + line: (stroke: config.colors.neutral-darkest)) + on-layer(1, { + circle((angle: 0deg, radius: 1), name: "a") + circle((angle: 90deg, radius: 1), name: "b") + circle((angle: 180deg, radius: 1), name: "c") + circle((angle: 270deg, radius: 1), name: "d") + circle((angle: 60deg, radius: 0.5), name: "x") + }) + line("a", "b", "c", "d", "a") + if 7 <= self.subslide { + line("a", "d", "c", "x", "a", fill: config.colors.primary.transparentize(20%)) + } + if 6 <= self.subslide { + line((angle: 0deg, radius: 1.5), (angle: 180deg, radius: 1.5), stroke: (paint: config.colors.primary, thickness: 1.5pt, dash: "dashed")) + } + }))), + uncover("8-10", align(center, cetz.canvas(length: 33%, { + import cetz.draw: * + + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05), + line: (stroke: config.colors.neutral-darkest)) + let xθ = 20deg + let yθ = xθ + 180deg + on-layer(1, { + circle((angle: 0deg, radius: 1), name: "a") + circle((angle: 120deg, radius: 1), name: "b") + circle((angle: 240deg, radius: 1), name: "c") + circle((angle: xθ, radius: 0.3), name: "x") + circle((angle: yθ, radius: 0.3), name: "y") + }) + line("a", "b", "c", "a") + if 9 <= self.subslide { + line((angle: xθ, radius: 1.5), (angle: yθ, radius: 1.5), stroke: (paint: config.colors.primary, thickness: 1.5pt, dash: "dashed")) + } + if 10 <= self.subslide { + line("a", "x", "y", "c", "a", fill: config.colors.primary.transparentize(20%)) + } + }))) + ) +]) + +== 9 points with no 5-holes + +#slide( + // Hide header by making it background-coloured + // config: config-colors(secondary: config.colors.neutral-lightest), + align: center+horizon, + repeat: 4, + self => cetz.canvas({ + import cetz.draw: * + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 1.2), + line: (stroke: config.colors.neutral-darkest)) + scale(.1) + on-layer(1, { + let pts = ( + (1, 0, "a"), + (100, 0, "b"), + (51, 88, "c"), + + (30, 40, "d"), + (49, 10, "e"), + (70, 40, "f"), + + (45, 26, "g"), + (55, 26, "h"), + (50, 35, "i"), + ) + + for (x, y, n) in pts { + circle((x, y), name: n) + } + }) + if self.subslide > 1 { + line("a", "b", "c", "a") + line("d", "e", "f", "d") + line("g", "h", "i", "g") + } + if self.subslide == 3 { + line("a", "e", "h", "i", "d", "a", fill: config.colors.primary-light.transparentize(20%)) + content((25, -10), [5-hole ✘]) + content((25, -20), [convex 5-gon ✔]) + } + if self.subslide == 4 { + line("d", "e", "b", "h", "g", "d", fill: config.colors.primary-light.transparentize(20%)) + content((75, -10), [convex 5-gon ✘]) + } +})) + +== The Happy Ending Problem + +#slide( + config: config-methods(cover: utils.semi-transparent-cover.with(alpha: 85%)), + self => [ + // WN: Not sure about this uncover dance.. + #uncover("1, 3, 5", [$g(k) =$ least $n$ s.t. any set of $n$ points must contain a *convex $bold(k)$-gon*]) + + #uncover("1, 2, 4, 5", [$h(k) =$ least $n$ s.t. any set of $n$ points must contain a *$bold(k)$-hole*]) + + #uncover("2, 5", [We just showed $h(4) ≤ 5$ and $9 < h(5)$]) + + #uncover("3, 5", [ + *Theorem* @35erdos_combinatorial_problem_geometry. + For a fixed $k$, every _sufficiently large_ set of points contains a convex $k$-gon. + So all $g(k)$ are finite. + ]) + + #uncover("4, 5", [ + *Theorem* @hortonSetsNoEmpty1983. + For any $k ≥ 7$, there exist arbitrarily large sets of points containing no $k$-holes. + So $h(7) = h(8) = … = ∞$. + ]) + ] +) + +== Known tight bounds + +#slide( + config: config-methods(cover: utils.semi-transparent-cover.with(alpha: 85%)), + repeat: 6, + self => [ + #let (uncover, only, alternatives) = utils.methods(self) + #let mkalt(s, k, n) = alternatives( + $#s (#k) = #n$, + $#s (#k) ≤ #n$, $#s (#k) ≤ #n$, $#s (#k) ≤ #n$, + $#(n -1) < #s (#k)$, + $#s (#k) = #n$ + ) + #let mkbnd(s, k, n, c) = [#mkalt(s, k, n) #set text(size: 15pt);#c] + #table( + columns: (1.3fr, 1fr), + inset: 6pt, + stroke: none, + mkbnd("h", 3, 3, [(trivial)]), + mkbnd("g", 3, 3, [(trivial)]), + mkbnd("h", 4, 5, [(Klein 1932)]), + mkbnd("g", 4, 5, [(Klein 1932)]), + mkbnd("h", 5, 10, [@Harborth1978]), + mkbnd("g", 5, 9, [(Makai 1930s)]), + [*#mkbnd("h", 6, 30, [@03overmars_finding_sets_points_empty_convex_6_gons @24heule_happy_ending_empty_hexagon_every_set_30_points])*], + mkbnd("g", 6, 17, [@szekeres_peters_2006]), + ) + + #uncover("1, 6", [We formally verified all the above in #lean.]) + + #uncover("2-4, 6", [Upper bounds by combinatorial reduction to SAT.]) + #[ + #set par(first-line-indent: 1em, hanging-indent: 1em) + #uncover("2, 6", [▸ We focused on $h(6)$, established this year.])\ + #uncover("3, 6", [▸ $g(6)$ previously verified in Isabelle/HOL @19maric_fast_formal_proof_erdos_szekeres_conjecture_convex_polygons_most_six_points.])\ + #uncover("4, 6", [▸ Efficient SAT encoding of Heule & Scheucher speeds up $g(6)$ verification.]) + ] + + #uncover("5, 6", [Lower bounds by checking concrete sets of points.]) + ] +) + +== SAT-solving mathematics + +#slide( + config: config-methods(cover: utils.semi-transparent-cover.with(alpha: 85%)), + repeat: 4, + self => [ + #let (uncover, only,) = utils.methods(self) + + #uncover("1, 3, 4", [ + *Reduction.* Show that a mathematical theorem is true + if a propositional formula φ is unsatisfiable. + ]) + + #uncover("1, 2, 4", [ + *Solving.* Show that φ is indeed unsatisfiable using a SAT solver. + ]) + + #uncover("2, 4", [ + ▸ Solving is reliable, reproducible, and trustworthy: + formal proof systems (DRAT) and verified proof checkers (`cake_lpr`). + ]) + + #uncover("3, 4", [ + ▸ But reduction is problem-specific, and involves complex transformations: + _focus of our work_. + ]) + ] +) + +#let reduction-slide(step) = [ +== Reduction from geometry to SAT +#slide( + config: config-methods(cover: utils.semi-transparent-cover.with(alpha: 85%)), + repeat: 1, + self => [ + #set text(size: 23pt) + #uncover(if step == 1 { "1" } else { "2" }, [ + 1. Discretize from continuous coordinates in $ℝ²$ to boolean variables. + ]) + #uncover(if step == 2 { "1" } else { "2" }, [ + 2. Points can be put in _canonical form_ + without removing $k$-holes. + ```lean + theorem symmetry_breaking {l : List Point} : + 3 ≤ l.length → PointsInGenPos l → + ∃ w : CanonicalPoints, l ≼σ w.points + ``` + ]) + #uncover(if step == 3 { "1" } else { "2" }, [ + 3. $n$ points in canonical form with no $6$-holes + induce a propositional assignment that satisfies $φ_n$. + ```lean + theorem satisfies_hexagonEncoding {w : CanonicalPoints} : + ¬σHasEmptyKGon 6 w → w.toPropAssn ⊨ Geo.hexagonCNF w.len + ``` + 4. But $φ_30$ is unsatisfiable. + ```lean + axiom unsat_6hole_cnf : (Geo.hexagonCNF 30).isUnsat + ``` + ]) + ] +)] + +#reduction-slide(1) + +== Discretization with triple-orientations + +#let fig = align(center, cetz.canvas({ + import cetz.draw: * + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.1)) + scale(3.2) + + on-layer(1, { + let pts = ( + (0, 0, "p"), (1, 1, "s"), (2, 1, "q"), (1.2, 2, "r"), (1.8, 1.8, "t") + ) + for (x, y, n) in pts { + circle((x, y), name: n) + content((x, y+0.015), [#set text(fill: config.colors.neutral-lightest, size: 20pt); $#n$]) + } + }) + + let (cg, cb, cr) = (green, blue, red).map(c => c.desaturate(20%)) + line("p", "r", "q", stroke: cg, mark: (end: "stealth", fill: cg)) + line("p", "s", "t", stroke: cb, mark: (end: "stealth", fill: cb)) + line("r", "s", "q", stroke: cr, mark: (end: "stealth", fill: cr)) +})) + +#components.side-by-side( + columns: (1fr, 18em), + fig, + [ + $ σ(p,r,q) &= 1 &("clockwise") \ + σ(p,s,t) &= 0 &("collinear") \ + σ(r,s,q) &= -1#h(1em) &("counter-clockwise") $ + ] +) #pause + +#align(center, [ + $∃$ $k$-hole ⇔ a propositional formula over $σ(a,b,c)$ is satisfiable +]) + +// WN: I think cap-cup here would be too deep into the weeds + +#reduction-slide(2) + +== Symmetry breaking + +#[ + #set text(size: 22pt) + *Lemma*. WLOG we can assume that the points $(p_1, ..., p_n)$ are in _canonical form_, meaning that they satisfy the following properties: + + ▸ *($x$-order)* The points are sorted with respect to their $x$-coordinates,\ i.e., $(p_i)_x < (p_j)_x$ for all $1 ≤ i < j ≤ n$. + + ▸ *(CCW-order)* All orientations $σ(p_1, p_i, p_j)$, with $1 < i < j ≤ n$, are counterclockwise. + + ▸ *(Lex order)* The first half of list of adj. orientations is lex-below the second half: + $ [σ(p_(⌈n/2⌉+1), p_(⌈n/2⌉+2), p_(⌈n/2⌉+3)), ..., σ(p_(n-2), p_(n-1), p_n)] succ.eq \ + [σ(p_(⌈n/2⌉−1), p_(⌈n/2⌉), p_(⌈n/2⌉+1)), ..., σ(p_2, p_3, p_4)] $ +] + +#slide(repeat: 6, align: center+horizon, self => [ + #let fig = cetz.canvas({ + import cetz.draw: * + let pts = ( + ((-1.3, 0.25), (-1.3, 0.9), (-0.7, -0.45), (-0.35, 0.35), (-0.35, -0.8), (0.6, 0.5), (0.9, -0.6), (1.4, 1.1), (0.6, -1.1),), + ((-1.09601563215555, -0.7424619411597272), (-1.5556349648261614, -0.28284245828783905), (-0.17677682816699475, -0.8131727694796578), (-0.49497474683057663, 8.087761060870946e-08), (0.3181979186635819, -0.8131728503572684), (0.07071080521204193, 0.7778174477512475), (1.0606602064416402, 0.21213186104679588), (0.21213232320457065, 1.767766918304512), (1.202081470247393, -0.3535535870103234),), + ((0.4596193326706113, -0.45961948287188814), (0.0, 0.0), (1.3788581366591666, -0.5303303111918187), (1.0606602179955846, 0.28284253916544966), (1.8738328834897433, -0.5303303920694293), (1.6263457700382034, 1.0606599060390867), (2.6162951712678018, 0.4949743193346349), (1.767767288030732, 2.0506093765923508), (2.7577164350735544, -0.07071112872248436),), + ((-1.00000032679495, 2.1757135283877527), (0, 3.85), (-0.3846155721840648, 0.7252377698715973), (0.2666664916498519, 0.9428090005013866), (-0.2830190444100679, 0.5336655199142649), (0.6521736801480853, 0.6148753963780468), (0.1891890199433349, 0.3822198699068886), (1.1599996167350177, 0.5656853177286622), (-0.025641189145902285, 0.3626188636662086),), + ((-1.00000032679495, 2.1757135283877527), (-1.2, 3.85), (-0.3846155721840648, 0.7252377698715973), (0.2666664916498519, 0.9428090005013866), (-0.2830190444100679, 0.5336655199142649), (0.6521736801480853, 0.6148753963780468), (0.1891890199433349, 0.3822198699068886), (1.1599996167350177, 0.5656853177286622), (-0.025641189145902285, 0.3626188636662086),), + ((-1.2, 3.85), (-1.00000032679495, 2.1757135283877527), (-0.3846155721840648, 0.7252377698715973), (-0.2830190444100679, 0.5336655199142649), (-0.025641189145902285, 0.3626188636662086), (0.1891890199433349, 0.3822198699068886), (0.2666664916498519, 0.9428090005013866), (0.6521736801480853, 0.6148753963780468), (1.1599996167350177, 0.5656853177286622),), + ) + let extents = ( + ((-1.7, -1.3), (1.7, 2.3)), + ((-1.7, -1.3), (1.7, 2.3)), + ((-0.7, -1.3), (3.1, 2.3)), + ((-1.2, -0.2), (2.4, 2.9)), + ((-1.5, -0.2), (2.4, 3.7)), + ((-1.5, -0.2), (2.4, 3.7)), + ) + let regions = ( + (("1", "3", "4", "2", "1"), ("3", "5", "9", "7", "6", "4", "3"), ("6", "7", "8", "6"), ("2", "4", "6", "8", "2"),), + (("1", "3", "4", "2", "1"), ("3", "5", "9", "7", "6", "4", "3"), ("6", "7", "8", "6"), ("2", "4", "6", "8", "2"),), + (("1", "3", "4", "2", "1"), ("3", "5", "9", "7", "6", "4", "3"), ("6", "7", "8", "6"), ("2", "4", "6", "8", "2"),), + (("1", "3", "4", "b", "a", "1"), ("3", "5", "9", "7", "6", "4", "3"), ("6", "7", "8", "6"), ("4", "6", "8", "c", "b", "4"),), + (("1", "3", "4", "2", "1"), ("3", "5", "9", "7", "6", "4", "3"), ("6", "7", "8", "6"), ("2", "4", "6", "8", "2"),), + (("1", "2", "3", "7", "1"), ("3", "4", "5", "6", "8", "7", "3"), ("6", "9", "8", "6"), ("7", "8", "9", "1", "7"),), + ) + + scale(3.2) + + // Grid and axes + let ((efx, efy), (etx, ety)) = extents.at(self.subslide - 1) + on-layer(-1, { + grid2( + (calc.ceil(efx), calc.ceil(efy)), (calc.floor(etx), calc.floor(ety)), + (efx, efy), (etx, ety), + stroke: (thickness: 0.2pt, paint: config.colors.secondary.transparentize(50%), dash: "dashed")) + }) + set-style(line: (stroke: (paint: config.colors.neutral-darkest, thickness: 1.5pt))) + line((efx, 0), (etx, 0), mark: (end: "stealth", fill: config.colors.neutral-darkest)) + line((0, efy), (0, ety), mark: (end: "stealth", fill: config.colors.neutral-darkest)) + content((etx -0.18, -0.2), $x$) + content((0.2, ety -0.1), $y$) + + // Points + on-layer(1, { + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.1)) + for (n, (x, y)) in pts.at(self.subslide - 1).enumerate(start: 1) { + if self.subslide == 4 and n == 2 { + // Point at infinity gets special color + circle((x, y), name: str(n), fill: config.colors.primary) + } else { + circle((x, y), name: str(n)) + } + content((x, y), [#set text(fill: config.colors.neutral-lightest, size: 20pt); #str(n)]) + } + }) + + // Convex regions + on-layer(-1, { + set-style(line: (stroke: none)) + let colors = (red, orange, blue, green).map(c => c.transparentize(30%)) + // Extra convex regions at infinity + if self.subslide == 4 { + circle((-1.00000032679495, 2.7), name: "a", radius: 0) + circle((0.2666664916498519, 2.7), name: "b", radius: 0) + circle((1.1599996167350177, 2.7), name: "c", radius: 0) + circle((-0.1, 3.4), name: "x", radius: 0) + circle((0, 3.4), name: "y", radius: 0) + circle((0.1, 3.4), name: "z", radius: 0) + line("x", "y", "2", "x", fill: colors.at(0)) + line("y", "z", "2", "y", fill: colors.at(3)) + line("a", "x", stroke: (thickness: 2pt, dash: "dotted", paint: colors.at(0))) + line("b", "y", stroke: (thickness: 2pt, dash: "dotted", paint: colors.at(0))) + line("c", "z", stroke: (thickness: 2pt, dash: "dotted", paint: colors.at(3))) + } + + for (r, c) in regions.at(self.subslide - 1).zip(colors) { + line(..r, fill: c) + } + }) + + // Equal-x marker lines + if self.subslide == 1 { + let ((_, yf), (_, yt)) = extents.at(0) + let (x4, _) = pts.at(0).at(3) + let (x6, _) = pts.at(0).at(5) + set-style(line: (stroke: (thickness: 2pt, dash: "dashed", paint: red))) + line((x4, yf), (x4, yt)) + line((x6, yf), (x6, yt)) + } + }) + + #let captions = ( + [Starting set of points.], + [Rotation ensures distinct $x$.], + [Translate leftmost point to $(0,0)$.\ + Ensures nonnegative $x$.], + [Map $(x,y) ↦ (y/x, 1/x)$.], + [Bring point at $∞$ back.], + [Relabel in order of increasing $x$.], + ) + + #components.side-by-side( + columns: (15em, 1fr), + captions.at(self.subslide - 1), + fig, + ) +]) + +// WN: Hid this slide, it doesn't add much +/* +== Symmetry breaking: result + +Points now in normal form. #pause + +Normalization drastically reduces search space for SAT solver. #pause + +```lean +structure CanonicalPoints where + leftmost : Point + rest : List Point + sorted' : (leftmost :: rest).Sorted (·.x < ·.x) + gp' : ListInGenPos (leftmost :: rest) + oriented : rest.Pairwise (σ leftmost · · = .ccw) + lex : σRevLex rest +``` +*/ + +#reduction-slide(3) + +== Running the SAT solver + +CNF formula produced directly from executable #lean definition. #pause + +To verify $h(6) ≤ 30$:\ #pause +▸ CNF with 65#(thin)092 variables and 436#(thin)523 clauses\ #pause +▸ partitioned into 312#(thin)418 subproblems\ #pause +▸ each subproblem solved by CaDiCaL 1.9.5\ #pause +▸ unsatisfiability proofs checked on-the-fly by `cake_lpr`\ #pause +▸ 25#(thin)876.5 CPU hours on Bridges 2 cluster of Pittsburgh Supercomputing Center + +== Lower bounds + +To prove $n < h(k)$, +find a set of $n$ points with no $k$-holes. #pause + +Naive checker algorithm is $cal(O)(n^(k+1)log k)$ time. #pause + +We verified an $cal(O)(n^3)$ solution\ +from #cite(<90dobkin_searching_empty_convex_polygons>, form: "prose"). + +== Hole-finding algorithm + +#slide(align: center+horizon, repeat: 7, self => cetz.canvas({ + import cetz.draw: * + + let radius = 0.2 + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: radius)) + set-style(line: (stroke: (thickness: 3pt))) + let pts = ( + ((-9, -2), (-5, 7)), + ((7, -4), (18, -3), (16, 0), (12, 1), (23, 3), (11, 3), (17, 8), (9, 5), (2, 4)) + ) + let (left, right) = pts.map(pts => pts.map(((x, y)) => (x/2,y))) + let chain = (0, 3, 5, 7, 8).map(i => right.at(i)) + for (x, y) in left { + circle((x, y), radius: if self.subslide > 1 { 0.15 } else { radius }) + } + if self.subslide == 7 { + line(..((0,0), ..chain), fill: aqua.transparentize(30%), stroke: none) + } + if self.subslide > 1 { + line((0, -4), (0, 8), stroke: (dash: "dashed", paint: config.colors.neutral-darkest)) + } + if self.subslide == 5 { + line(right.at(0), right.at(3), stroke: (dash: "dashed", paint: aqua, thickness: 4pt)) + line(right.at(4), right.at(7), stroke: (dash: "dashed", paint: red, thickness: 4pt)) + } + if self.subslide == 6 { + line(..chain, stroke: (dash: "dashed", paint: aqua, thickness: 4pt)) + } + for (n, (x, y)) in ((0,0), ..right).enumerate() { + if self.subslide > 3 { + let (nx, ny) = if n < right.len() { right.at(n) } else { (0, 0) } + let thick = if self.subslide == 6 and n == 8 { 1pt } else { 4pt } + line((x, y), (nx, ny), stroke: (paint: config.colors.neutral-darkest, thickness: thick)) + } + if n != 0 { + if self.subslide == 3 { + line((x, y), (0, 0), stroke: (paint: config.colors.neutral-darkest)) + } + circle((x, y), name: str(n), radius: if self.subslide > 1 { 0.3 } else { radius }) + if self.subslide > 2 { + content((x, y), [#set text(fill: config.colors.neutral-lightest, size: 20pt); #str(n)]) + } + } + } + circle((0, 0), name: "p", radius: if self.subslide > 1 { 0.4 } else { radius }) + if self.subslide > 1 { + content((0, .13 /* HACK */), [#set text(fill: config.colors.neutral-lightest, size: 20pt); $p$]) + } +})) + +== Hole-finding algorithm: verification + +#align(center, [ +#image("./proof.png") #pause +expands to #pause +#[#set text(size: 15pt) +```lean +theorem of_proceed_loop + {i j : Fin n} (ij : Visible p pts i j) {Q : Queues n j} {Q_j : BelowList n j} {Q_i} (ha) + {IH} (hIH : ∀ a (ha : a < i), Visible p pts a j → ProceedIH p pts (ha.trans ij.1) (IH a ha)) + (Hj : Queues.OrderedTail p pts lo j (fun k h => Q.q[k.1]'(Q.sz ▸ h)) Q_j.1) + (ord : Queues.Ordered p pts lo i (fun k h => Q.q[k.1]'(Q.sz ▸ h.trans ij.1)) Q_i) + (g_wf : Q.graph.WF (VisibleLT p pts lo j)) + {Q' Q_j'} (eq : proceed.loop pts i j ij.1 IH Q Q_j Q_i ha = (Q', Q_j')) : + ∃ a Q₁ Q_i₁ Q_j₁, proceed.finish i j ij.1 Q₁ Q_i₁ Q_j₁ = (Q', Q_j') ∧ + Q₁.graph.WF (VisibleLT p pts i j) ∧ + (∀ k ∈ Q_i₁.1, σ (pts k) (pts i) (pts j) ≠ .ccw) ∧ + lo ≤ a ∧ Queues.Ordered p pts a i (fun k h => Q.q[k.1]'(Q.sz ▸ h.trans ij.1)) Q_i₁.1 ∧ + (∀ (k : Fin n) (h : k < j), ¬(lo ≤ k ∧ k < a) → Q₁.q[k.1]'(Q₁.sz ▸ h) = Q.q[k.1]'(Q.sz ▸ h)) ∧ + Queues.OrderedTail p pts a j (fun k h => Q₁.q[k.1]'(Q₁.sz ▸ h)) Q_j₁.1 := by +``` +] +]) + +== Lower bound: 29 points with no 6-holes @03overmars_finding_sets_points_empty_convex_6_gons + +#slide( + // Hide header by making it background-coloured + // config: config-colors(secondary: config.colors.neutral-lightest), + align: center+horizon, + repeat: 2, + self => cetz.canvas({ + import cetz.draw: * + set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 1.2), + line: (stroke: config.colors.neutral-darkest)) + scale(.1) + let pts = ( + (1.2, ((1-10, 1260+10), (37-10, 0-10), (1259+10, 320))), + (1.2, ((16, 743), (22, 531), (777, 194), (754, 697))), + (1.2, ((306, 592), (310, 531), (371, 487), (516, 467), (552, 502), (496, 579), (396, 613))), + (1.0, ((366, 552), (374, 525), (450, 498), (492, 502), (489, 537), (446, 565), (392, 575))), + (0.8, ((410, 539), (426, 526), (449, 518), (458, 526), (453, 542), (434, 552), (416, 550))), + (0.9, ((436, 535),)), + ) + on-layer(1, { + for (i, (radius, cycle)) in pts.enumerate() { + for (j, (x, y)) in cycle.enumerate() { + circle(((y+x/4)/5, x/11), radius: radius, name: str(i)+"-"+str(j)) + } + } + }) + if self.subslide > 1 { + for (i, (_, cycle)) in pts.enumerate() { + let cycle = range(cycle.len()) + cycle.push(0) + line(..cycle.map(x => str(i)+"-"+str(x))) + } + } +})) + +== Final theorem + +#[ +#set text(size: 24pt) +```lean +axiom unsat_6hole_cnf : (Geo.hexagonCNF 30).isUnsat + +theorem holeNumber_6 : holeNumber 6 = 30 := + le_antisymm + (hole_6_theorem' unsat_6hole_cnf) + (hole_lower_bound [ + (1, 1260), (16, 743), (22, 531), (37, 0), (306, 592), + (310, 531), (366, 552), (371, 487), (374, 525), (392, 575), + (396, 613), (410, 539), (416, 550), (426, 526), (434, 552), + (436, 535), (446, 565), (449, 518), (450, 498), (453, 542), + (458, 526), (489, 537), (492, 502), (496, 579), (516, 467), + (552, 502), (754, 697), (777, 194), (1259, 320)]) +``` +] + +== Conclusion + +We used Lean to fully verify a recent result in combinatorial geometry +based on a sophisticated reduction to SAT. #pause + +Upper and lower bounds for all finite _hole numbers_ $h(k)$ +followed with additional effort. #pause + +Open problems remain: + +▸ Horton's construction of $h(k) = ∞$ for $7 ≤ k$ hasn't been verified. #pause + +▸ Exact values of $g(k) < ∞$ for $7 ≤ k$ aren't known. #pause + +▸ Trust story for large SAT proofs could be improved. + +== Bibliography + +#bibliography("main.bib", style: "chicago-author-date", title: none) diff --git a/flake.lock b/flake.lock index fd85f3d..9b66e4e 100644 --- a/flake.lock +++ b/flake.lock @@ -5,11 +5,11 @@ "systems": "systems" }, "locked": { - "lastModified": 1705309234, - "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=", + "lastModified": 1710146030, + "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", "owner": "numtide", "repo": "flake-utils", - "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26", + "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", "type": "github" }, "original": { @@ -20,11 +20,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1705883077, - "narHash": "sha256-ByzHHX3KxpU1+V0erFy8jpujTufimh6KaS/Iv3AciHk=", + "lastModified": 1725534445, + "narHash": "sha256-Yd0FK9SkWy+ZPuNqUgmVPXokxDgMJoGuNpMEtkfcf84=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "5f5210aa20e343b7e35f40c033000db0ef80d7b9", + "rev": "9bb1e7571aadf31ddb4af77fc64b2d59580f9a39", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index cd8760d..d106b60 100644 --- a/flake.nix +++ b/flake.nix @@ -16,6 +16,7 @@ fontconfig gcc python3 + typst ]; FONTCONFIG_FILE = pkgs.makeFontsConf { fontDirectories = [