Search the scholarly object
Find works by prose, Lean name, topic, person, project, source module, and eventually dependency or citation graph.
About Therefore
A scholarly layer for formal mathematics.
Therefore is designed to make Lean work discoverable and citable without confusing repository activity, mathematical authorship, or machine verification.
Say exactly what was checked
Project-declared completion is distinct from an independent rebuild, axiom audit, expert statement review, or Mathlib upstreaming.
Preserve immutable versions
A verification record pins the commit, Lean toolchain, dependency lock, build result, omissions, and custom axioms.
Keep provenance with every claim
Imported titles, authorship, links, abstracts, licenses, and statuses retain their source and assertion method.
What therefore is and is not
Mathlib documentation, Loogle, LeanSearch, LeanExplore, and Reservoir already provide excellent declaration or package discovery. Therefore does not try to replace them. It connects formal artifacts to researchers, projects, publications, versions, sources, and roles.
A GitHub contributor is not automatically a proof author. An import is not automatically a citation. Stars are not scholarly impact. Therefore keeps those signals separately labeled until there is evidence for a stronger relationship.
Unclaimed profiles are seeded only from explicit repository, project, citation, or public identity evidence. Ownership requests are manually reviewed; profile photos are user-provided rather than copied from arbitrary websites.