Skip to content
View Peiyang-Song's full-sized avatar
38 followers · 49 following

Achievements

Achievement: YOLOAchievement: QuickdrawAchievement: Starstruckx3Achievement: Pull Sharkx2

Achievements

Achievement: YOLOAchievement: QuickdrawAchievement: Starstruckx3Achievement: Pull Sharkx2

Highlights

  • Pro

Organizations

@ucsb @lean-dojo
Block or Report

Block or report Peiyang-Song

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
Peiyang-Song/README.md
  • 👋 I am an undergraduate student studying Computer Science at California Institute of Technology (Caltech). I am a researcher in the Computation & Cognition Lab (CoCoLab) at Stanford University, advised by Prof. Noah Goodman.
  • 🔎 My current research interest is in machine reasoning, especially AI for mathematics. During the past, I have also worked on energy-efficient machine learning systems.
  • ❤️ I have been fortunate to work with Prof. Anima Anandkumar (Caltech), Dr. Kaiyu Yang (Meta), Prof. Tim Sherwood (UC Santa Barbara), and Dr. Jeremy Lau (Google) during my undergrad.
  • 📫 I'm always open to collaborations. Please feel free to email me at [email protected].

Pinned Loading

  1. lean-dojo/LeanCopilot lean-dojo/LeanCopilot Public

    LLMs as Copilots for Theorem Proving in Lean

    C++ 863 77

  2. lean-dojo/LeanDojo lean-dojo/LeanDojo Public

    Tool for data extraction and interacting with Lean programmatically.

    Python 485 72

  3. lean-dojo/ReProver lean-dojo/ReProver Public

    Retrieval-Augmented Theorem Provers for Lean

    Python 193 40

  4. lean-dojo/LeanDojoWebsite lean-dojo/LeanDojoWebsite Public

    Code for LeanDojo's website

    JavaScript 7 1

  5. LLM-A-Not-B-Errors LLM-A-Not-B-Errors Public

    Official repository for paper "In-Context Learning May Not Elicit Trustworthy Reasoning: A-Not-B Errors in Pretrained Language Models"

    Python 2

  6. zhaoyu-li/DL4TP zhaoyu-li/DL4TP Public

    [COLM 2024] A Survey on Deep Learning for Theorem Proving

    96 5