Skip to content
View digama0's full-sized avatar
440 followers · 0 following

Achievements

Achievement: Pair Extraordinairex4Achievement: Starstruckx3Achievement: QuickdrawAchievement: YOLOAchievement: Pull Sharkx3Achievement: Arctic Code Vault Contributor

Achievements

Achievement: Pair Extraordinairex4Achievement: Starstruckx3Achievement: QuickdrawAchievement: YOLOAchievement: Pull Sharkx3Achievement: Arctic Code Vault Contributor

Organizations

@metamath @leanprover-community

Block or report digama0

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse

  • HOL Public

    Forked from HOL-Theorem-Prover/HOL

    Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

    Standard ML Other Updated Dec 11, 2024

  • hol4-vscode Public

    Forked from HOL-Theorem-Prover/hol4-vscode

    HOL4 mode for VSCode

    TypeScript 1 Updated Dec 7, 2024

  • equational_theories Public

    Forked from teorth/equational_theories

    A project to map out the relations between different equational theories of Magmas.

    Lean Apache License 2.0 Updated Dec 4, 2024

  • mm0 Public

    Metamath Zero specification language

    Lean 324 40 Creative Commons Zero v1.0 Universal Updated Nov 25, 2024

  • lean4 Public

    Forked from leanprover/lean4

    Lean 4 programming language and theorem prover

    Lean Apache License 2.0 Updated Nov 19, 2024

  • lean4checker Public

    Forked from leanprover/lean4checker

    Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel.

    Lean 1 1 Apache License 2.0 Updated Nov 4, 2024

  • lean4lean Public

    Lean 4 kernel / 'external checker' written in Lean 4

    Lean 78 7 Updated Nov 2, 2024

  • leangz Public

    Lean 4 .olean file (de)compressor

    Rust 5 1 Apache License 2.0 Updated Nov 1, 2024

  • dae-parser Public

    Rust crate for parsing Collada DAE files

    Rust 10 Apache License 2.0 Updated Oct 4, 2024

  • minidom-14 Public

    Rust 1 1 Mozilla Public License 2.0 Updated Oct 4, 2024

  • digama0.github.io Public

    My personal website

    HTML 1 Updated Sep 30, 2024

  • polyml Public

    Forked from polyml/polyml

    Poly/ML

    Standard ML GNU Lesser General Public License v2.1 Updated Sep 23, 2024

  • mmj2 Public

    mmj2 GUI Proof Assistant for the Metamath project

    Java 72 26 GNU General Public License v2.0 Updated Sep 16, 2024

  • mm-hammer Public

    A tool for automatically proving Metamath theorems using ATPs

    Rust 10 2 Updated Sep 12, 2024

  • isabelle-rs Public

    Parser for isabelle database files

    Rust Updated Sep 1, 2024

  • isabelle Public

    Fork of https://isabelle-dev.sketis.net so I can use git

    Isabelle Other Updated Sep 1, 2024

  • oleandump Public

    A type-aware olean tparser for Lean 4 olean files

    Lean 3 1 Updated Aug 20, 2024

  • mizar-rs Public

    Alternative Mizar proof checker (http://mizar.org/) written in Rust

    Rust 48 4 GNU General Public License v3.0 Updated Aug 3, 2024

  • ast_export Public

    AST export from Lean 4

    Lean 8 Apache License 2.0 Updated Jul 25, 2024

  • coq Public

    Forked from coq/coq

    Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…

    OCaml GNU Lesser General Public License v2.1 Updated Jul 24, 2024

  • lean-sys Public

    Rust bindings for the Lean 4 proof assistant

    Rust 19 6 Apache License 2.0 Updated Jun 18, 2024

  • FLT Public

    Forked from ImperialCollegeLondon/FLT

    Ongoing Lean formalisation of the proof of Fermat's Last Theorem

    TeX 1 Apache License 2.0 Updated Jun 16, 2024

  • mm-web-rs Public

    A metamath web site generator in rust

    HTML 5 Creative Commons Zero v1.0 Universal Updated Apr 23, 2024

  • LeanSAT Public

    Forked from FormalSAT/trestle
    Lean Apache License 2.0 Updated Apr 16, 2024

  • LeanColls Public

    Forked from JamesGallicchio/LeanColls

    WIP collections library for Lean 4

    Lean Apache License 2.0 Updated Apr 15, 2024

  • vscode-lean4 Public

    Forked from leanprover/vscode-lean4

    Visual Studio Code extension for the Lean 4 proof assistant

    TypeScript Apache License 2.0 Updated Mar 20, 2024

  • lean-rs Public

    High level Lean 4 FFI for Rust

    Rust 13 1 Updated Mar 16, 2024

  • moonrider Public

    Forked from supermedium/moonrider

    🌕🏄🏿 Surf the musical road among the stars. Side project built by two people in a few months to demonstrate WebXR.

    JavaScript MIT License Updated Mar 3, 2024

  • verbose-lean4 Public

    Forked from PatrickMassot/verbose-lean4

    Natural language tactics to teach mathematics using Lean 4

    Lean 1 Apache License 2.0 Updated Feb 15, 2024

  • bors-ng Public

    Forked from robertylewis/bors-ng

    👁 A merge bot for GitHub Pull Requests

    Elixir Apache License 2.0 Updated Jan 12, 2024