diff --git a/projects/Aya/sample.md b/projects/Aya/sample.md
new file mode 100644
index 0000000000000000000000000000000000000000..263a55ad4e14199d41809536a59f0eb626a40fa1
--- /dev/null
+++ b/projects/Aya/sample.md
@@ -0,0 +1,31 @@
+
+1. 项目名称：Aya
+
+2. 项目图标：
+
+![](https://raw.githubusercontent.com/aya-prover/aya-prover-docs/main/src/public/logo.svg)
+
+3. 项目主页：<https://www.aya-prover.org>
+
+4. 项目仓库：<https://github.com/aya-prover/aya-dev>
+
+5. 项目简介。
+
+Aya 语言的特色是它强大的类型系统。这个类型系统拥有『依值类型（dependent type）』、『参数化多态（polymorphism）』这两个功能，
+且支持等号类型。换言之，「两个值相等」这件事是一个类型，而它的实例就是这两个值相等的证明。
+例如，`插入排序 = 归并排序` 是一个合法的类型，且它等价于函数 `(x : 列表) -> 插入排序(x) = 归并排序(x)`,
+也就是接收一个列表、返回它被两种排序算法排序后结果相同的证明。这样的证明可以在编程的同时证明一些关于程序的性质。
+
+在 Aya 团队的招募贴 <https://github.com/lazyparser/weloveinterns/blob/master/bunbun.md> 中，
+有更详细的项目动机介绍。
+
+有关 Aya 中语言特性的学术论文参见 <https://www.aya-prover.org/pubs> 这个页面。
+
+6. 项目分类：免费、开源（MIT）、通用、接受社区贡献  
+语言类别：高级编程语言、函数式语言、多范式语言  
+工具类别：类型检查器、解释器，实时编译器尚未完成。另外有官方维护的编辑器插件的服务端  
+应用领域：通用、行业应用、计算数学。更具体来说，有编写算法类的程序、开发编译器、形式化数学等应用  
+
+7. 联系方式: ice1000kotlin@gmail.com（电子邮箱）
+
+> 注：以上文档使用5号字体，A4幅面排版时，总篇幅不超过3页，最终版式参考"sample.doc"。
\ No newline at end of file