Skip to content
View xukp20's full-sized avatar
馃幍
Coding
馃幍
Coding
29 followers · 37 following
  • Beijing

Achievements

Achievement: YOLOAchievement: Pull Sharkx2

Achievements

Achievement: YOLOAchievement: Pull Sharkx2

Highlights

  • Pro

Block or report xukp20

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.

Maximum 250 characters. Please don鈥檛 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鈥檚 behavior. Learn more about reporting abuse.

Report abuse
xukp20/README.md

Hi, I'm Jerry 馃憢

Building reliable infrastructure for AI agents, formal reasoning, and scientific discovery.

Agent Infrastructure 聽路聽 Lean & Formalization 聽路聽 Scientific AI

What I build

Agent Infrastructure

Provider-neutral runtimes, durable state, typed orchestration, and practical tooling for coding agents. 		Lean & Formalization

Agent-assisted proof engineering, reusable Lean tooling, and formalization aligned with mathematical sources. 		Scientific AI

Reproducible environments and observation-grounded benchmarks for scientific modeling and design agents.

Featured projects

Agent Runtime Kit

A durable, provider-neutral runtime contract for heterogeneous coding agents, typed workflows, and restorable state.

Python Agent Runtime Orchestration

Repository 路 Documentation

SciModelingBench

Observation-grounded benchmarks for scientific modeling and design agents, with reproducible datasets, objectives, protocols, and evaluation.

Python Scientific AI Benchmarking

Repository 路 PyPI 路 Datasets

Lean MCP Toolkit

A unified Lean tool server exposing diagnostics, LSP, search, and declaration tools through MCP, HTTP, CLI, and local shell interfaces.

Lean 4 MCP Formal Methods

Repository 路 Documentation

Lean Constellation In development

Exploring multi-agent workflows for Lean formalization and proof engineering.

Lean 4 Multi-Agent Proof Engineering

Public details coming soon.

All we see is sky for forever.

Pinned Loading

  1. prompt-scratchpad prompt-scratchpad Public

    A lightweight VS Code scratchpad for drafting prompts and sending them to Codex or Claude Code in the terminal.

    TypeScript 2

  2. agent-runtime-kit agent-runtime-kit Public

    A lightweight Python runtime kit for provider-backed agents, with agent type templates, isolated homes, scoped thread snapshots, and simple orchestration primitives.

    Python 1

  3. sci-modeling-bench sci-modeling-bench Public

    An observation-grounded benchmark framework for scientific modeling and design, with reusable datasets, queryable objectives, and task protocols.

    Python 1