Smale's sixth problem for five bodies in the plane, with a proof formalized in Lean
Every choice of five positive masses gives finitely many planar central configurations, up to similarity.
Papers
Selected papers
The rank of 3×3 matrix multiplication over F2 is 23
Laderman's algorithm uses the fewest multiplications among all bilinear algorithms over F2.
Operon Finder: A Deep Learning-based Web Server for Accurate Prediction of Prokaryotic Operons
A web server that predicts operons in prokaryotic genomes with a deep-learning model.
Sorting networks on 13 inputs need at least 44 comparators
Raises the proved lower bound for 13 inputs from 43 to 44 comparators.
Area law for three-dimensional U(1) lattice gauge theory with the Wilson action at every coupling
Three-dimensional U(1) lattice gauge theory with the Wilson action confines static charges at every coupling.
Uniqueness of four-body convex central configurations for all masses
For any four positive masses and any cyclic ordering of the bodies there is exactly one strictly convex central configuration with that ordering, up to similarity.
More papers
Smale's sixth problem for six bodies in the plane: finiteness of central configurations for generic masses, with a proof formalized in Lean
Finiteness for six bodies in the plane at generic masses, outside a proper algebraic subset of the mass space.
A formal proof in Lean of the finiteness of planar central configurations of five bodies
The Lean 4 and Mathlib formalization of the five-body theorem, checked by the kernel and by two independent kernels.
The number of planar central configurations of four bodies
The number of four-body central configurations for all masses outside a closed null set: always even, between 32 and 50.
Complex solution sets of the planar five-body problem at special masses
Explicit complex solution sets at three special mass vectors, one of which carries a continuum of complex solutions. Finiteness at these masses follows without counting.
A resource-efficient deep learning framework for pest and disease detection in plants
A lightweight MobileNetV2-based model that identifies plant pests and diseases, optimized to run on Android.