# orderedItems[].object.content
@ykonstant There have been several discussions on Zulip about the Jordan curve theorem or combinatorial maps / plane maps / planar graphs (and possible approaches for formalizing them), but so far none of those discussions have resulted in someone formalizing any of those things.

# orderedItems[].object.contentMap.en
@ykonstant There have been several discussions on Zulip about the Jordan curve theorem or combinatorial maps / plane maps / planar graphs (and possible approaches for formalizing them), but so far none of those discussions have resulted in someone formalizing any of those things.

# orderedItems[].object.content
@ykonstant For formalizing Appendix A in isolation, yes, piecewise linear would suffice, and for more general spectres in the second paper, piecewise 𝐶¹ would suffice. The goal of my formalization is to get everything into either mathlib or the mathlib archive, which means doing it in appropriate generality rather than just more limited versions needed for a particular application. For example, if anything depends on the basic division of the boundary of a tile (in a locally finite tiling by closed topological disks) into vertices and edges - Statements 3.1.1, 3.1.2 and 3.1.3 of Tilings and Patterns - then those should be formalized in general, not just for tiles with well-behaved boundaries.

# orderedItems[].object.contentMap.en
@ykonstant For formalizing Appendix A in isolation, yes, piecewise linear would suffice, and for more general spectres in the second paper, piecewise 𝐶¹ would suffice. The goal of my formalization is to get everything into either mathlib or the mathlib archive, which means doing it in appropriate generality rather than just more limited versions needed for a particular application. For example, if anything depends on the basic division of the boundary of a tile (in a locally finite tiling by closed topological disks) into vertices and edges - Statements 3.1.1, 3.1.2 and 3.1.3 of Tilings and Patterns - then those should be formalized in general, not just for tiles with well-behaved boundaries.

# orderedItems[].object.content
It's now one year from the release of "An aperiodic monotile" preprint. That year has seen an amazing outflow of mathematical and artistic work building on the hat, turtle and spectre aperiodic monotiles, and I'm very much looking forward to seeing what the future brings! In an update on the original work, "An aperiodic monotile" was accepted by a journal in December and is now awaiting publication, while a revised version of "A chiral aperiodic monotile", addressing referee comments on the first version, was submitted last month. I've started preparations for the Lean formalization of both papers and expect to continue with more substantive work on that formalization after IMO 2024; I don't think there will be any particular difficulties in formalizing the purely combinatorial parts of the arguments, but the link between the combinatorial and geometrical views of the tiles (Appendix A of "An aperiodic monotile") is likely to be rather more time-consuming to formalize (note that mathlib doesn't yet have either the Jordan curve theorem, which is likely to be of use, or Euler's theorem for plane maps, which is definitely needed).

# orderedItems[].object.contentMap.en
It's now one year from the release of "An aperiodic monotile" preprint. That year has seen an amazing outflow of mathematical and artistic work building on the hat, turtle and spectre aperiodic monotiles, and I'm very much looking forward to seeing what the future brings! In an update on the original work, "An aperiodic monotile" was accepted by a journal in December and is now awaiting publication, while a revised version of "A chiral aperiodic monotile", addressing referee comments on the first version, was submitted last month. I've started preparations for the Lean formalization of both papers and expect to continue with more substantive work on that formalization after IMO 2024; I don't think there will be any particular difficulties in formalizing the purely combinatorial parts of the arguments, but the link between the combinatorial and geometrical views of the tiles (Appendix A of "An aperiodic monotile") is likely to be rather more time-consuming to formalize (note that mathlib doesn't yet have either the Jordan curve theorem, which is likely to be of use, or Euler's theorem for plane maps, which is definitely needed).

# orderedItems[].object.content
Thanks to everyone who came to remember Vicky Neale and celebrate her life in Oxford today!

# orderedItems[].object.contentMap.en
Thanks to everyone who came to remember Vicky Neale and celebrate her life in Oxford today!

# orderedItems[].object.content
@tao We do have numerical bounds on 𝑒 (Mathlib.Data.Complex.ExponentialBounds) and it's certainly possible to prove numerical bounds on powers (I have a Lean 3 example attached to https://leanprover.zulipchat.com/#narr ow/stream/208328-IMO-grand-challenge/topic/IMO.202020/near/212247641 ) - but, yes, it's much more complicated than it should be (people have talked about wanting a single tactic to prove such things automatically by numerical approximation).

# orderedItems[].object.contentMap.en
@tao We do have numerical bounds on 𝑒 (Mathlib.Data.Complex.ExponentialBounds) and it's certainly possible to prove numerical bounds on powers (I have a Lean 3 example attached to https://leanprover.zulipchat.com/#narr ow/stream/208328-IMO-grand-challenge/topic/IMO.202020/near/212247641 ) - but, yes, it's much more complicated than it should be (people have talked about wanting a single tactic to prove such things automatically by numerical approximation).

# orderedItems[].object.content
"TIME Magazine Best Inventions of 2023" is not something I expected for a pure mathematics preprint! https://time.com/collection/best-inven tions-2023/6324101/the-einstein-shape/

# orderedItems[].object.contentMap.en
"TIME Magazine Best Inventions of 2023" is not something I expected for a pure mathematics preprint! https://time.com/collection/best-inven tions-2023/6324101/the-einstein-shape/

# orderedItems[].object.content
@OscarCunningham @ColinTheMathmo Allowing some numbers to be left unused is one of the features I added to my code to apply it to this problem (the other was supporting the constraint of only integer intermediates). There are cases such as {9, 9, 10, 10, 25, 75} where you can make 777 = (9 / 25 + 10) * 75 with four of the numbers but can't do it with only integer intermediates even using all six (I don't know if there are any like that that can make the target with fewer than four of the numbers, the choice of which representation my code logged is arbitrary, not necessarily using the fewest possible of the numbers).

# orderedItems[].object.contentMap.en
@OscarCunningham @ColinTheMathmo Allowing some numbers to be left unused is one of the features I added to my code to apply it to this problem (the other was supporting the constraint of only integer intermediates). There are cases such as {9, 9, 10, 10, 25, 75} where you can make 777 = (9 / 25 + 10) * 75 with four of the numbers but can't do it with only integer intermediates even using all six (I don't know if there are any like that that can make the target with fewer than four of the numbers, the choice of which representation my code logged is arbitrary, not necessarily using the fewest possible of the numbers).

# orderedItems[].object.content
@ColinTheMathmo The smallest target number (I haven't checked for target numbers below 101) is 103 = ((1 + 5) / 50 + 5 - 1) * 25 = 5 * (25 - (1 - 6 / 50) * 5) = 75 / (10 - 10 / 6) + 100 - 6. Next smallest is 105 = (8 - 2 / 4) * (2 + 4 + 8) = 10 * (1 / (9 / 9 + 1) + 10). The multiset {1, 1, 8, 50, 75, 100} has 188 such target numbers, starting with 120 = 100 / (1 - 75 / (1 + 8) / 50) and ending with 996 = 8 * ((1 - 1 / 100) * 50 + 75). The nine T with no such M are 101, 102, 104, 108, 111, 125, 150, 300, 600.

# orderedItems[].object.contentMap.en
@ColinTheMathmo The smallest target number (I haven't checked for target numbers below 101) is 103 = ((1 + 5) / 50 + 5 - 1) * 25 = 5 * (25 - (1 - 6 / 50) * 5) = 75 / (10 - 10 / 6) + 100 - 6. Next smallest is 105 = (8 - 2 / 4) * (2 + 4 + 8) = 10 * (1 / (9 / 9 + 1) + 10). The multiset {1, 1, 8, 50, 75, 100} has 188 such target numbers, starting with 120 = 100 / (1 - 75 / (1 + 8) / 50) and ending with 996 = 8 * ((1 - 1 / 100) * 50 + 75). The nine T with no such M are 101, 102, 104, 108, 111, 125, 150, 300, 600.

# orderedItems[].object.content
@ColinTheMathmo There are 13243 multisets of six integers satisfying the given rules. Putting all 13243 multisets through code I have for such puzzles, I reckon that 10012 of them have at least one integer in the range 101 to 999 that can be reached only with non-integer intermediates (one multiset has 188 such integers); all but nine of the integers in that range have at least one such multiset that can reach that integer but only with non-integer intermediates; there are 115373 (multiset, integer) pairs with this property.

# orderedItems[].object.contentMap.en
@ColinTheMathmo There are 13243 multisets of six integers satisfying the given rules. Putting all 13243 multisets through code I have for such puzzles, I reckon that 10012 of them have at least one integer in the range 101 to 999 that can be reached only with non-integer intermediates (one multiset has 188 such integers); all but nine of the integers in that range have at least one such multiset that can reach that integer but only with non-integer intermediates; there are 115373 (multiset, integer) pairs with this property.

# orderedItems[].object.content
@moultano @csk I think there's a theorem that for any aperiodic set of tiles (that tiles with finitely many possible local configurations and with tiles appearing in finitely many orientations, at least) it's not possible to produce a tiling purely by applying local rules: you should always expect to need backtracking.

# orderedItems[].object.contentMap.en
@moultano @csk I think there's a theorem that for any aperiodic set of tiles (that tiles with finitely many possible local configurations and with tiles appearing in finitely many orientations, at least) it's not possible to produce a tiling purely by applying local rules: you should always expect to need backtracking.

# orderedItems[].object.content
@Geosynchronicity If all the angles between those segments are sufficiently close to 180 degrees, so that there are no new possibilities for how tiles fit together at a vertex, that certainly works; we just don't have a proof for the general case of a completely arbitrary curve without any such restriction on angles, so only state things in the paper for the 𝐶¹ case.

# orderedItems[].object.contentMap.en
@Geosynchronicity If all the angles between those segments are sufficiently close to 180 degrees, so that there are no new possibilities for how tiles fit together at a vertex, that certainly works; we just don't have a proof for the general case of a completely arbitrary curve without any such restriction on angles, so only state things in the paper for the 𝐶¹ case.