By improving upon previous estimates on a problem posed by L. Moser, we prove a conjecture of Erdős that the density of any measurable planar set avoiding unit distances is less than 1/4. Our argument implies the upper bound of 0.2470.

Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search.

What fraction of the plane can be colored so that two colored points cannot be exactly a unit distance away from each other? This geometric question was formulated by Leo Moser in the early 1960s. According to a conjecture of Paul Erdős, this fraction must be less than ¼. The currently best lower bound of 0.2293 is given by a construction by Hallard Croft dating back to 1967. Several research groups have published partial results on the problem, gradually strengthening the initial upper density estimate of 0.

In this work, we present our reproducibility study of Label-Free Explainability for Unsupervised Models, a paper that introduces two post‐hoc explanation techniques for neural networks: (1) label‐free feature importance and (2) label‐free example importance. Our study focuses on the reproducibility of the authors’ most important claims: (i) perturbing features with the highest importance scores causes higher latent shift than perturbing random pixels, (ii) label‐free example importance scores help to identify training examples that are highly related to a given test example, (iii) unsupervised models trained on different tasks show moderate correlation among the highest scored features and (iv) low correlation in example scores measured on a fixed set of data points, and (v) increasing the disentanglement with β in a β‐VAE does not imply that latent units will focus on more different features.