About Cryptography Academy

Vision

cryptography.academy is an open knowledge base for cryptographic research literature. We process papers from the cryptographic research corpus, extract every definition, theorem, lemma, and formula, and cross-reference them across the entire body of literature. When Paper A cites a definition from Paper B, we link them. When two papers define the same concept differently, we surface it. When a proof relies on a property established elsewhere, we trace it back to its source.

Think of it as a compiler for cryptographic literature: just as a compiler checks that every reference in your code resolves correctly, cryptography.academy verifies that every reference in the research resolves, is consistent, and is traceable to its origin.

The long-term goal is formal verification. Definitions and theorems extracted from papers are progressively formalized in Lean 4, building a machine-checked foundation for cryptographic knowledge — starting with zero-knowledge-proof-optimized primitives like Poseidon and the algebraic structures they depend on.

No other tool operates at this level of granularity. Citation graphs link papers to papers. We link definitions to definitions, formulas to formulas, and proofs to the precise results they depend on — across the entire cryptographic literature.

This project is and will always be free. No profit is made, no knowledge will ever be sold, and there will never be a paywall. We act in good faith, respect intellectual property, and welcome feedback from authors and the community. The entire source code is publicly available. Read the full vision statement.

Future Scope

While we start with cryptography, the platform is designed to expand into a broader mathematics.academy covering:

  • Physics and mathematical physics
  • Geometry (algebraic, differential, computational)
  • Financial mathematics and quantitative finance
  • Machine learning and AI foundations
  • Category theory and abstract algebra

Developed By

BaDaaS

A research laboratory in mathematics based in Belgium, focused on formal methods, cryptography, and privacy-preserving technologies.

Danny Willems

"A mathematician fighting for privacy and security on the Internet, while dreaming about describing the Universe with equations and symbols."

Contributing

Contributions are welcome! Whether you want to:

  • Formalize a new theorem
  • Improve existing proofs
  • Write educational content
  • Create visualizations
  • Fix bugs or typos

Check out our GitHub repository to get started.

License

This project is released under the MIT License. The Lean formalizations and website content are freely available for educational and research purposes.