Runnel Zhang (Runcheng Zhang)

Email: Runnel.Zhang@smail.nju.edu.cn | GitHub: @ChouYuanjue | ORCID: 0009-0005-7611-3583

Education

Nanjing University | Nanjing, Jiangsu, CN

B.S. in Intelligent Science and Technology | Sep 2025 – Present

Research Intern | TsinghuaNLP (AI4S Research Group)

Advisor: Prof. Zheni Zeng | Mar 2026 - Present

Focus on the intersection of artificial intelligence and scientific discovery (AI4Sci), specializing in the application of large language models to complex scientific reasoning and active learning domains.

External Collaborator | Microsoft Research Asia (MSRA)

Collaborator: Ziyu Zhou | Jan 2026 – Present

Partner on specialized AI for Mathematics (AI4Math) research initiatives, bridging advanced pure mathematical frameworks with modern machine learning paradigms.
Architect and develop Mathub, an AI-integrated collaborative platform for mathematical knowledge management and project execution.

Core Developer (PoC Phase) | Bank of Nanjing

Multimodal LLM-based Customer Emotion Recognition System | Jan 2026 – Mar 2026

Designed and implemented an AI-powered system for analyzing customer emotions in complex banking environments.

Full-Stack Engineer | FluxVerse

Core Engineering Team | Jan 2026 - Present

Developing comprehensive full-stack solutions, ensuring robust architectural design and seamless integration of complex engineering projects.

Core Member & Teaching Assistant | NJU Artificial Intelligence Association (AIA)

Academic & Technical Group | Sep 2025 – Present

Organize and lead academic sharing sessions focusing on foundational AI theories and practical implementations.
Scheduled to deliver a core lecture on Variational Autoencoders (VAE), designing hands-on experimental cases to bridge theoretical math with model applications. Provide targeted guidance on Python and ML fundamentals.

Core Member | NJU NOVA (Intelligent Data Decision Studio)

Engineering Group | Sep 2025 – Jan 2026

Directed technical solutions for multi-source information aggregation projects, developing core backend modules and ensuring high integration efficiency.
Delivered formal lectures on full-stack development, covering front-end/back-end synchronization and enterprise-level engineering practices.

Tangut-NLP: Ultra-Low-Resource Tangut Translation

Studied short-text Tangut-to-Chinese translation under an extremely small parallel set, focusing on the gap between dictionary-grounded prompting, local training, and hybrid candidate selection.
Built evaluation and analysis utilities for reference-aware scoring, contamination checks, uncertainty analysis, and frontier/local workflow comparison.

Lean Portfolio Attribution

GitHub: ChouYuanjue/lean-portfolio-attribution

Built an experimental framework for attributing inference-time gains in Lean proving, separating effects from attempt scheduling, retrieval, compute budget, and prover-specific behavior.
Implemented fixed-budget portfolio experiments, retrieval-free and matched-compute controls, and portability checks against external prover baselines.

CORAL Travel Planning

GitHub: ChouYuanjue/coral-travel-planner

Developed a travel-planning evaluation pipeline centered on raw-query grounding and localized repair, targeting executable plans rather than prompt-only plausibility.
Added benchmark adapters, repair audits, ceiling-aware reporting, infeasibility checks, and run manifests for TravelPlanner and ChinaTravel experiments.

ProCo: Missing-Support Witnesses for Indexed Rule Reasoning

Investigated proof-style reasoning with three evidence regimes: proving entailed queries, refuting contradicted queries, and abstaining on unsupported queries with missing-support witnesses.
Built data processing, training, evaluation, verifier, and analysis scripts around ProofWriter-style open-world reasoning, emphasizing checkable evidence rather than raw-label accuracy alone.

Rzk/sHoTT Autoformalization Experiments

GitHub: ChouYuanjue/rzk-ai4math

Used Rzk/sHoTT body-completion tasks as a low-resource autoformalization setting for auditing substrate bias, structural priors, verifier-grounded repair, and shape-heavy definition failures.
Added extraction, evaluation, replay, failure-taxonomy, task-complexity, and Lean portability probes to make model failures more inspectable across formal substrates.

Zhang, R. (2025). Navigating the Full-Stack Ecosystem: Implementation Strategies and Knowledge Graphs for Information Aggregation. Zenodo Lecture. DOI: 10.5281/ZENODO.17852269.
Zhang, R. (2025). Architectural Paradigms in Collaborative Software Engineering: A Comprehensive Analysis of the Nova Project. Zenodo Lecture. DOI: 10.5281/ZENODO.17765724.
Zhang, R. (2023). Gravitational Fields of Non-Spherical Mass Distributions: Analysis and Orbital Dynamics. DOI: 10.6084/M9.FIGSHARE.22268917.
Zhang, R. (2023). On the Factorization of Cyclotomic-Type Polynomials $\sum_{i=0}^k x^{in}$ and Their Divisibility Properties. Preprint. DOI: 10.6084/M9.FIGSHARE.22268908.

National 2nd Prize, CCF Certified Software Professional (Senior Level) | 2023
National 2nd Prize, National High School Mathematics Olympiad (Preliminary) | 2024
Provincial 1st Prize, National High School Mathematics League | 2024
Provincial 1st Prize, National High School Biology League | 2024
Selected Participant, Peking University Winter School (2025) & Summer School (Yuanpei College, 2024) for Outstanding High School Students