Fredrik Johansson

Stream: new members

[Fredrik Johansson]

Not a Lean user (yet), just an interested observer.

One of my pet project ideas for some time is to have a repository of formally encoded definitions, formulas and theorems for special functions. I created https://fungrim.org to explore this idea. Nothing is formally certified, though. I'll be interested in seeing how special_functions in mathlib develops :smiling_face:

[Huỳnh Trần Khanh]

Is it like OEIS, but for functions?

[Mario Carneiro]

How does it compare to the NIST Digital Library of Mathematical Functions, which I think evolved from Abramowitz & Stegun?

[Fredrik Johansson]

DLMF is more of a classical reference work using text + latex while Fungrim is a database of context-free and computer-readable symbolic expressions, with explicit "assumptions" (explicitly quantified variables). This should make it possible to export the data to computer algebra systems and theorem provers. As I said, I have not done any formal verification, but I have been able to test about 75% of the formulas using an automated framework which plugs in random values satisfying the assumptions and checks consistency using a combination of symbolic computation and complex interval arithmetic. There is a brief paper here: https://arxiv.org/abs/2003.06181

[Fredrik Johansson]

Huỳnh Trần Khanh said:

Is it like OEIS, but for functions?

OEIS is OEIS for functions. You just have to find the right way to interpret your function as an integer sequence :smile: