Problem with creating new Lean project

Stream: new members

[Tom Leung]

Hi, when I try to create a new project, I encounter the following error:

trace: creating lean-action CI workflow
trace: created lean-action CI workflow at '.\.github\workflows\lean_action_ci.yml'
trace: .> git init -q
info: downloading mathlib lean-toolchain file
trace: .> curl -s -S -f -o .\lean-toolchain -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain
trace: stderr:
curl: (35) schannel: next InitializeSecurityContext failed: CRYPT_E_NO_REVOCATION_CHECK (0x80092012) - The revocation function was unable to check revocation for the certificate.
error: external command 'curl' exited with code 35
error: failed to download mathlib 'lean-toolchain' file; you can manually copy it from:
{mathToolchainUrl}

Does anyone have idea on how to solve this?

[Ruben Van de Velde]

You can manually download the file from https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain and put it in the root of your repository

[Ruben Van de Velde]

What command did you run?

[Tom Leung]

lake new myproject math

[Tom Leung]

Once I put the file there how can I continue the process?

[Tom Leung]

Anyways, seems that even if I create a new project using the VS Code method, it encounter the same error.
I tried a fresh install in a different computer and still have the same problem.

[Ruben Van de Velde]

Can you find out your curl version?

[Tom Leung]

how to find out curl version?
Sorry that I am not too familiar with coding.

[Tom Leung]

Oh I found out now:

curl 8.14.1 (x86_64-w64-mingw32) libcurl/8.14.1 Schannel zlib/1.3.1 brotli/1.1.0 zstd/1.5.7 libidn2/2.3.8 libpsl/0.21.5 libssh2/1.11.1
Release-Date: 2025-06-04
Protocols: dict file ftp ftps gopher gophers http https imap imaps ipfs ipns ldap ldaps mqtt pop3 pop3s rtsp scp sftp smb smbs smtp smtps telnet tftp ws wss
Features: alt-svc AsynchDNS brotli HSTS HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM PSL SPNEGO SSL SSPI threadsafe UnixSockets zstd