Utensil's Projects
A collection of tools for writing technical documents that mix Coq code and prose.
We extend CoT data to Alpaca to boost its reasoning ability. We are constantly expanding our collection of instruction-tuning data, and integrating more LLMs together for easy use. (我们将CoT数据扩展到Alpaca以提高其推理能力,同时我们将不断收集更多的instruction-tuning数据集,并在我们框架下集成进更多的LLM,打造一个通用的LLM-IFT平台。)
A curated list of my GitHub stars!
Go ahead and axolotl questions
Proof of concepts for C/C++ backend server architectures.
A book to gather and distill principles, patterns and templates behind programming.
Personal checklist for setting up a development environment. Inspired by mdo/config
:whale: Dockerfiles https://hub.docker.com/u/utensil/
An simplified implementation of TCP, based on UDP(not raw packet), written in Erlang, for personal study purpose only.
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
This is a mirror of https://git.sr.ht/~jonsterling/forester-base-theme for https://github.com/utensil/forest, created because of hours of service interuption of SourceHut on Jun 17, 2024.
A Lean file formatter
A work-in-progress Lean 4 binding to GiNaC
⟨Grassmann-Clifford-Hodge⟩ multilinear differential geometric algebra
Geometric algebra library for Rust.
Hierarchical Temporal Memory implementation in Java - a Community-Driven Java port of the Numenta Platform for Intelligent Computing (NuPIC).
Citations in Hugo websites.
A widget to show a Github user's basic info and repositories, written as a jQuery plugin.
A series of experiments with Julia and Python
Coding assistance for JupyterLab (code navigation + hover suggestions + linters + autocompletion + rename) using Language Server Protocol
Lean Prover Cheat Sheet
A partial formalization of Geometric Algebra in the Lean formal proof verification system.
Lean 4 language server wrapper for Jupyter LSP
Experiment with Lean prover.