Robert Joseph Claim this profile

Learning in infinite dimension with neural operators.

CLRS(Introduction to Algorithms) - Python/C++/Java Implementation of all the major Algorithms in the CLRS Textbook as well as additional algorithm's covered in the University of Alberta theory Courses

A collection of formalized statements of conjectures in Lean.

Mathematics + Statistics Courses at the University of Alberta

Notebooks , Machine Learning Algorithms and Notes

A uv-inspired project, dependency, cache, and toolchain manager for Lean

Lean statements, proofs, and audits for the AIM AINT 2026 problem list

NKIPy: Rapid Prototyping on Trainium

Lean 4 formalization accompanying a candidate partial solution to Erdős Problem 634

No description.

Weekly TorchLean examples with checked Lean proofs, CUDA certificates, and reproducible ML verification demos.

No description.

alpha-beta-CROWN: An Efficient, Scalable and GPU Accelerated Neural Network Verifier (winner of VNN-COMP 2021, 2022, 2023, 2024, 2025)

Statistics in Lean

Header files for Lean 4 theorem provers — separate what is true from why it is true

🚧 Accepting Task Submissions 🚧

No description.

No description.

No description.

The math library of Lean 4

A collection of optimization problems in mathematics

The Lean Computer Science Library (CSLib)

ICERM Workshop

Implementation of all the Numerical Algorithms covered in the textbook (A first course on numerical methods) as well as additional Algorithms taught at the University of Alberta.

[Re] D-CODE: Discovering Closed-form ODEs from Observed Trajectories