Skip to content
View siqiliu-tsinghua's full-sized avatar

Block or report siqiliu-tsinghua

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.

Content in all repositories owned by your account will be closed.
Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. Markdown is supported. This note will only be visible to you.
Report abuse

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

Report abuse

Popular repositories Loading

  1. mma-mcp mma-mcp Public archive

    A MCP server that wraps a local Wolfram Engine, enabling AI assistants (Claude, ChatGPT, etc.) to perform symbolic math, numerical analysis, and data visualization via Wolfram Language.

    Python 32 2

  2. tautology tautology Public

    Real analysis formalized in Lean 4 from nothing — the reals are constructed here. No mathlib, no external dependencies, no typeclasses.

    Lean 27 1

  3. mma-hol mma-hol Public

    A kernel-minimal LCF-style HOL theorem prover in the Wolfram Language

    Wolfram Language 10

  4. rum rum Public

    An embeddable, sandbox-first symbolic term-rewriting language and runtime in Rust — exact rational arithmetic and a capability sandbox for safely evaluating untrusted scripts.

    Rust 4

  5. Li2Rational Li2Rational Public

    Lean 4 proofs of the irrationality of Li₂(r) at certain rational points r

    Lean 3

  6. qiao qiao Public

    Self-hosted bridge that exposes a local stdio MCP server to the ChatGPT and Claude connectors over HTTPS with OAuth.

    Python 1