LMFDB / lmfdb

L-Functions and Modular Forms Database
Other
246 stars 200 forks source link

Certifying completeness of search results #3989

Open AndrewVSutherland opened 4 years ago

AndrewVSutherland commented 4 years ago

One of the great features of the Jones-Roberts number field database is that it will tell you when the set of results is provably complete (i.e. every number field that satisfies the criteria you have specified is included). This is an extremely valuable feature (it allows you to prove theorems, not just find examples).

It would be great if we could provide a similar service to parts of the LMFDB where it is feasible to do so. Local and global number fields would be obvious candidates, as would Dirichlet characters, elliptic curves, CMFs, HMFs, BMFs, and abelian varieties over finite fields (genus 2 curves, on the other hand, would be pretty hopeless).

A possible prerequisite for doing this is storing information in the database that gives a computational explicit description of the scope of the data that is present. For CMFs there is a mf_boxes table that does this.

This issue is potentially vast in scope and likely to never be completely accomplished, but that is no reason not to implement what we can when we can. It would probably make sense to pick a particular section where this might be easier to implement because the search parameters are fairly limited and the completeness of the data is easy to describe; possibly Dirichlet characters or local fields would be good candidates.

bmatschke commented 4 years ago

To add a suggestion: For the user it would be furthermore great to know why the search result is complete. For example if one searches for global number fields, the search result page could state: "This table is provably complete. (more)", and if one clicks on "more", the user could find a list of all complete families of fields that contain the search result, with precise descriptions of their scope and references (which should include proofs and the code that was used in the computation of the table).