Abstract: We focus on inspiring people to formalize new proofs in LEAN by formalizing a few topics in topology that are not yet formalized. Modern mathematical proofs are known for their huge size and complexity, and have reached a level at which peer review by humans is increasingly challenged. As the size and sophistication of proofs continue to grow, human verification alone becomes increasingly challenging. Subtle errors may remain undetected despite extensive peer review. Since mathematical correctness is vital, researchers have increasingly turned to computer-assisted proof verification. Interactive proof verification software such as Lean provides a rigorous framework in which every step can be checked mechanically, virtually mitigating the possibility of error. Lean is a functional programming language and theorem prover built to formalize mathematical proofs and formal verification. It is free open-source software developed by Microsoft Research in 2013 as an initial effort to help mathematicians and engineers express the proof in a precise formal language.
Abstract: Cataracts are one of the leading causes of vision impairment worldwide, and their burden is disproportionately concentrated in low-resource settings such as rural communities. Many existing state-of-the-art deep learning models for cataract detection struggle to localize the clinically relevant region, the pupil and instead learn spurious correlations with irrelevant features such as skin color and eyebrow texture. In this work, it is proposed that cataract grading can be improved by restricting model input to the pupil region and addressing two systematic data quality issues: scale variability and specular reflection artifacts. We developed a two-path preprocessing pipeline that applies partial convolution-based inpainting to remove bright spot artifacts and randomized zoom augmentation via a MONAI pipeline to normalize scale. A ResNet-18 classifier is then trained on pupil-cropped images to perform six-class cataract grading (No Cataract, NS1–NS5). Experiments demonstrate that the combined training strategy, mixing inpainted and non-inpainted images with data augmentation, achieves the best multi-class AUC of 0.8919. It is observed that the model reliably distinguishes healthy from cataractous eyes, while confusion between adjacent intermediate grades (NS2–NS3) remains a challenge for future work.
Equivariant Image Recognition with Matrix Groups: Symmetry Alignment, Steerable Filters, and Non-Euclidean Classification Heads
Abstract: Convolutional neural networks trained on raw image data must implicitly learn that an object is the same object regardless of its orientation, a burden that wastes model capacity and degrades sample efficiency. Group-equivariant convolutional networks (G-CNNs) address this by encoding geometric symmetries directly into the network architecture, guaranteeing that a transformation of the input produces a predictable, structured transformation of every intermediate feature map. In this work we study symmetry groups of increasing richness , C2, p4, p4m, and a steerable C8 backbone, and evaluate their effect on classification accuracy and parameter efficiency on the CIFAR-10 and CIFAR-100 benchmarks under a strictly controlled parameter budget. We implement the G-CNN framework of Cohen & Welling, a C8-steerable backbone via the e2cnn library, and a hyperbolic convolutional network that couples the best-performing equivariant backbone with a Poincaré ball classification head, motivated by the approximate tree-like structure of natural-image class hierarchies. Our central finding is that the value of a symmetry group is conditional on the dataset: the dihedral group p4m is the best equivariant model on CIFAR-10, where the data’s reflection symmetry aligns with the architectural constraint, while the rotation-only group p4 is best on CIFAR-100, where the additional dihedral constraint provides no benefit at a one-hundred-class budget. Equivariance consistently matches or exceeds the translation-only baseline at equal parameter count, and at matched training compute exceeds it by eight to nine percentage points on CIFAR-10. The hyperbolic classification head reaches parity with its Euclidean counterpart on CIFAR-10 but regresses by twelve points on CIFAR-100, contradicting parity reported in prior work at substantially larger backbone capacity and suggesting that the competitiveness of the hyperbolic head is capacity-dependent. Together, these results argue that geometric inductive biases must be matched to both the symmetry structure of the labels and the capacity of the backbone, rather than adopted as universal improvements.
Seg-Cat: Automatic Pupil Detection from Healthy and Cataract Patients
Abstract: Cataract is among the leading causes of vision impairment worldwide, affecting approximately 94 million individuals who often lack access to timely diagnostic services. Early detection is critical to preventing irreversible vision loss. This paper presents Seg-Cat, a pupil segmentation pipeline designed to address a key limitation of current State-of-the-Art (SOTA) models: the tendency to focus on irrelevant visual features such as skin colour and eyebrow texture rather than the medically relevant pupil region. Seg-Cat employs classical image processing techniques alongside deep learning segmentation using a U-Net architecture, with novel shape-aware loss functions to enforce anatomically consistent pupil boundaries. Experimental results demonstrate that incorporating geometric regularisers (circular and elliptical loss) into the U-Net training objective yields significant improvements over the baseline, achieving a Test Dice score of 0.931 and IoU of 0.871 with the circular variant.