A proof via finite elements for Schiffer's conjecture on a regular pentagon (Q827006)

The authors show that there exists a Neumann eigenfunction on a regular pentagon that is positive on the boundary and not identically constant. The proof of this result consists in blending ideas from analysis, optimization and numerical analysis (approximation theory techniques), and it is an interesting contribution in its own right. The proof itself is human-readable and fully analytic except for the matrix eigenvalue computations on 20 large matrices from the strategy for computing discrete eigenvalues and from the lower bound estimation for the smallest eigenvalue of a sparse matrix. The excepted part is of course a computed assisted proof. The authors have found a rather short proof certificate for this computed proof, show that it is checkable and adaptable.