Paid studies to formalize math problems in Lean

Stream: general

[Bulhwi Cha]

Samara Zauhy said:

There is a lot of demand for participants with Lean knowledge.

Can you tell us more about this? How many people want to pay Lean users to formalize math problems?

[Samara Zauhy]

Hey @Bulhwi Cha, thanks for your question!

Some of our biggest partners are keen to work with Lean users because of its applicability as a theorem prover. They plan to launch numerous studies that require participants to have either a working or expert knowledge of Lean 3.

Our understanding is, the more participants fulfil that knowledge criteria on the platform, the more studies they'll be able to publish. We can't share more specific details on a public forum, but hope that you choose to sign up and view the studies to see if they are are of interest.

[Filippo A. E. Nuccio]

Hi @Samara Zauhy can you describe a bit this platform, its commercial model, shareholders, etc?

[Samara Zauhy]

Hey @Filippo A. E. Nuccio,

Prolific is a private limited company in the UK. We provide a pool of vetted participants for researchers looking to get fast and high-quality responses to their studies.

When researchers publish a study on Prolific, they are charged a percentage over the amount they wish to pay participants. The minimum reward allowed is $8.00 an hour, and participants get to keep 100% of that amount, with the option of instant cash-out via PayPal.

[Alex Keizer]

I got interested and signed up, then got a bit wary when it asked me about a lot of personal details like country of birth, ethnicity and sex, and finally it seems I will have to verify these details by uploading a passport or ID card? It all seems a bit suspicious if indeed you're just interested in crowd-sourced Lean knowledge

[Samara Zauhy]

Hey @Alex Keizer, thanks for raising your concerns!

Prolific asks details such as country of birth, ethnicity and sex because researchers generally need a specific group of people for their studies, so they apply screeners based on the demographic information participants provide. For example, they may need male German residents, between the ages of 18 and 25. This information does not identify you in any way, it just means you will qualify for certain studies, so we'll know to send them your way!

The reason we ask for passport details or ID card is so we can verify our participants are real people, and not bots, or the same person creating multiple accounts. We verify the authenticity of that documentation using a software called Onfido, and that information is absolutely confidential, and only used for the purpose of verifying the authenticity of your account. This is quite an important step because it ensures that the data our researchers collect from the platform is coming from real people.

All data provided to us, both by researchers and participants, are protected under the General Data Protection Regulation (GDPR), this applies to special categories of data, such as race, ethnic origin, politics, religion, health, sex life or sexual orientation.

I hope this is helpful, but please don't hesitate to follow up with any questions or further concerns!

[Johan Commelin]

Why are bots not allowed to compete? Isn't that the end goal after all?
I would be surprised if they can make any money on the platform, given the state of the art. But ruling them out seems a bit pessimistic.

[Alex Keizer]

Sure, asking about these details makes sense for studies where they are relevant. I just fail to see why it's relevant for Lean studies. You mention GDPR, and I am not a lawyer, but I do know that according to Dutch law, only certain organizations (banks, employers, and the like) are allowed to ask for a copy of ID. I don't know whether this applies to foreign organizations, but it at least should tell you this requirement is a bit shady.

[Eric Wieser]

Johan Commelin said:

Why are bots not allowed to compete?

Presumably this is an anti-abuse mechanism; someone creating 100 anonymous bot accounts that answer every survey with "I don't know" is much harder to deal with than a single abusive user who runs the same bot through their verified account.

[Andrew Souther]

Hi everyone. I thought I might have a unique perspective on this thread. In undergrad, I used to contribute to mathlib (and I still like to follow news about Lean, so I check this channel occasionally). But now I work in economics research at a US government institution. I've used Prolific before as a researcher to conduct online behavioral economics experiments.

From the perspective of behavioral science research, Prolific is a relatively well-respected platform. Other similar platforms are basically overrun with bots to the point that they're unusable to recruit participants for psychology and economics surveys. So we value that Prolific is a place to find attentive and thoughtful research participants.

I'm not a Prolific rep or anything, but I wanted to offer my perspective because I think it's interesting the platform is now being used to study Lean.

[Samara Zauhy]

Alex Keizer said:

Sure, asking about these details makes sense for studies where they are relevant. I just fail to see why it's relevant for Lean studies. You mention GDPR, and I am not a lawyer, but I do know that according to Dutch law, only certain organizations (banks, employers, and the like) are allowed to ask for a copy of ID. I don't know whether this applies to foreign organizations, but it at least should tell you this requirement is a bit shady.

Thanks for raising this! KYC is also a requirement for organisations other than banks if they transmit money (for AML purposes). Since participants at Prolific get remunerated for their time, the business falls under that category as well.

The ID documents you provide at the onboarding stage are only temporarily held. In other words, we do not keep that information in our database. We use it only as a means to identify users in a compliant way, with a 3rd party provider.

On requesting demographic information, you're absolutely right - ethnicity and nationality information aren't an explicit requirement for Lean 3 studies per say, but it's the minimum screening information we need from users when they join our participant pool. That is because, once you claim your account, you will be automatically eligible for studies based on your basic demographic information.

For instance, if a researcher sets up a study with a US rep sample, we'd send their study to the all users in our participant pool who fit that demographic. Having that information from participants also helps us prevent them from being screened out of studies, as every study that arrives for them will have been pre-screened.

[Samara Zauhy]

Johan Commelin said:

Why are bots not allowed to compete? Isn't that the end goal after all?
I would be surprised if they can make any money on the platform, given the state of the art. But ruling them out seems a bit pessimistic.

That's a very interesting point! @Eric Wieser answered it quite well, so I will just build on their answer:

Not having participants who are (or are using) bots is one of the steps we take to uphold the high data quality standards of the platform, as bot-like responses aren't good quality ones. After all, researchers trust Prolific because of the quality of our participants.

Of course, there are many other aspects that contribute to "poor data" - unengaged participants will provide similarly poor data and, on a slightly different scale, participants who are over-exposed to manipulation and no longer naïve, may also provide poor data. So, while bots aren't the only problem, they are arguably the lowest bar for ensuring data quality in crowdsourcing platforms!

[Samara Zauhy]

Hey Lean enthusiasts! :space_invader:  We now have several Lean formalization tasks paying £25/hr, which are likely to continue for the next few months.

You can claim your account on the platform and start taking part in tasks **HERE**. This is an exclusive link that allows you to bypass our signup waitlist.

Once you’ve verified your account, which is super quick and easy, you can take as many studies as you want.

Any questions, feel free to reply to this thread or send me a message directly!

[Tomaz Gomes]

anyone has done it and can confirm that it's legit?

[Kevin Buzzard]

Some people on the Xena Discord have spoken highly about this opportunity (and in particular it is certainly legit)

[Anne Baanen]

Let me reiterate that it is not at all clear to me why you need this detailed demographic information for your studies. The platform may very well have legitimate interest in this data, but your studies apparently do not. I'm extremely concerned that you decided to use this platform that exposes your participants to potential harm.

[Anne Baanen]

Oh sorry, @Samara Zauhy, I understood you were organising the studies, but actually on re-reading the thread I believe you are affiliated with Prolific. Is that latter one correct? In that case I apologise, since I should have complained to the study organisers.

[Peter Li]

Samara Zauhy said:

Hey Lean enthusiasts! :space_invader:  We now have several Lean formalization tasks paying £25/hr, which are likely to continue for the next few months.

You can claim your account on the platform and start taking part in tasks **HERE**. This is an exclusive link that allows you to bypass our signup waitlist.

Once you’ve verified your account, which is super quick and easy, you can take as many studies as you want.

Any questions, feel free to reply to this thread or send me a message directly!

I'm from the US, could I still sign up?

[Samara Zauhy]

Anne Baanen said:

I'm extremely concerned that you decided to use this platform that exposes your participants to potential harm.

Hey Anne - thank you for raising your concerns! I'm indeed a representative for Prolific and not a study organiser. However, I want to reassure you that Prolific is deeply committed to protecting the anonymity and data of all participants who join our platform.

In part, what that means is that a participant will never be requested to provide identifiable information to a researcher. Aside from Lean 3 and programming tasks, Prolific is largely used to carry out academic research. As such, to sign up to our platform, we ask demographic information from all of our users. This allows researchers to run studies with a balanced demographic sample.

Hope this helps address your concerns, but please feel to reach out to me through here or privately on DM! :smile:

[Samara Zauhy]

@Peter Li Yes, you can! :smile:

We accept participants from most OECD countries, with the exception of Turkey, Lithuania, Colombia, Slovakia and Costa Rica where Prolific is not available.

[Eric Rodriguez]

that is a wild set of exceptions

[Julian Berman]

Your email confirmation link also does not use TLS (It's a plain HTTP URL). Besides that some browsers (like mine) will entirely block any HTTP traffic by default, it's almost certainly a good idea not to use such a redirect if you're mentioning you're about to collect passport or driver's license info.

[Yaël Dillies]

My ID verification failed for some reason. Am I effectively forever banned from the platform?

[Kyle Miller]

The platform doesn't seem to support people who aren't currently in the country of their nationality. I can't be American in Paris, and I'd guess you can't be French in Cambridge.

[Kyle Miller]

These requirements seem to make some sense for the usual use of Prolific, where you want accurate demographic information for studies, but it's certainly an odd quirk when it comes to being a platform looking for Lean users to formalize things. I was told that they're working on it.

[Andrés Goens]

Kyle Miller said:

The platform doesn't seem to support people who aren't currently in the country of their nationality. I can't be American in Paris, and I'd guess you can't be French in Cambridge.

Hm, it did work for me (I'm a non-UK citizen on the UK) :thinking: but I don't remember the details of the form tbh

[Alex J. Best]

Kyle Miller said:

The platform doesn't seem to support people who aren't currently in the country of their nationality. I can't be American in Paris, and I'd guess you can't be French in Cambridge.

I know of other people using it who are non-uk citizens in the UK too, so I don't think its as simple as that.
I also failed some sort of verification (UK citizen in UK), and sent them some emails to which they said they wouldn't reconsider, but after a week they manually reviewed my account and reinstated me though :shrug:.

[Filippo A. E. Nuccio]

I seem to be able to work with Prolific living in France with an Italian citizenship. But this is EU-EU :flag_european_union: (probably irrelevant, though). On the other hand, is the lean webeditor working for you? Currently, even the basic
https://leanprover-community.github.io/lean-web-editor/
does not compile for me.

[Eric Wieser]

@Filippo A. E. Nuccio, there is a thread about the web editor here. Optimistically, it should be live again after the next build.

[Eric Rodriguez]

the mathlib commit they are targetting is e8638a0fcaf73e4500469f368ef9494e495099b3, for people who want to use VSCode instead of the web editor

[Samara Zauhy]

Hey @Julian Berman, thanks for flagging! Can you let me know which link you're referring to? We can look into it!

[Filippo A. E. Nuccio]

@Samara Zauhy On of the other problems is that the studies are meant to be done online, and the web editor is broken. Having the commit allows to work locally on VSCode.

[Julian Berman]

Samara Zauhy said:

Hey Julian Berman, thanks for flagging! Can you let me know which link you're referring to? We can look into it!

It was a link that looked like http://url2476.prolific.co/ls/click?upn=<big base64 blob> from the Join Prolific button in this initial email:

Screenshot-2023-05-31-at-11.04.40.png

[Samara Zauhy]

@Julian Berman Oh I see what you mean! This is actually a https link, but for some reason when I scroll by it (not click it) it does show me a regular http url, as you said.

This is the actual link the button takes you to: https://app.prolific.co/participant/onboarding/complete

Were you able to open it in your browser or was it blocked? If it was, this is something I can bring back to the team and try to sort out.

[Samara Zauhy]

@Filippo A. E. Nuccio Thanks for letting me know - is this a problem you're experiencing when taking Lean studies on the platform? If so, happy to bring it up to the researcher and see what we can do!

[Filippo A. E. Nuccio]

Yes, indeed (I sent an e-mail both to the researcher and to your team), but Eric's is probably the solution.

[Samara Zauhy]

Thanks for sharing @Kyle Miller! :smile: You can definitely sign up if your nationality doesn't match your country of residence. When sign up fails at that stage, it's usually because of VPN use, or when there's a general mismatch in IP address and a phone number's country code.

We are however looking at further refining our security system to make sure participants who travel a lot and/or use VPN are able to safely use of the platform without getting flagged.

[Julian Berman]

Samara Zauhy said:

Julian Berman Oh I see what you mean! This is actually a https link, but for some reason when I scroll by it (not click it) it does show me a regular http url, as you said.

This is the actual link the button takes you to: https://app.prolific.co/participant/onboarding/complete

Were you able to open it in your browser or was it blocked? If it was, this is something I can bring back to the team and try to sort out.

That means it redirects to some HTTPS link afterwards -- but in the meanwhile someone's visiting an HTTP link and say, someone on the same public network might be able to see (and perhaps decode whatever's in that base64 blob, I didn't really try to see whether anything interesting was being sent back and forth in it), or someone on some malicious network can redirect your domain to some other place such that it never ends up at the HTTPS place you expect someone to land.

But for me personally yeah, I'm able to override the HTTP block.

[Notification Bot]

38 messages were moved here from #announce > Paid studies to formalize math problems in Lean by Scott Morrison.

[Ziyu Zhou]

@Samara Zauhy Hi I just successfully signed up for the account, but I didn't see the study about Lean on the page, just some unrelated studies.mmexport1686587479930.png

[Tom Rodenby]

Hey @Ziyu Zhou , Tom here (I work with Samara - she's out this week). I've added you to the eligible group today, so you should now see the study on your dashboard. Let me know if not! I'm also happy to be contacted via tom.rodenby@prolific.co if that's easier.

[Ziyu Zhou]

Tom Rodenby said:

Hey Ziyu Zhou , Tom here (I work with Samara - she's out this week). I've added you to the eligible group today, so you should now see the study on your dashboard. Let me know if not! I'm also happy to be contacted via tom.rodenby@prolific.co if that's easier.

Thank you! But unfortunately my account has just been suspended. It's strange, I'm Chinese, recently in China but usually in Norway, and I don't know why an account that has been successfully registered is prompted "We can't verify your ID". Please forgive me for complaining that your system places too many restrictions on users.

[Junyan Xu]

https://twitter.com/random_walker/status/1672254675679166465

[Samara Zauhy]

Hello! :wave: For everyone that has tried to sign up to Prolific or have any questions about the process, I am attaching my email so you can reach out on there if preferred: samara.zauhy@prolific.co

We still have Lean 3 studies running on the platform and paying £25/hr. If you're still interested in joining you can sign up using this link.

If you have signed up and still have any questions or need support, please feel free to contact me via email or on this stream! :smile:

[Eric Rodriguez]

(it's 40/hr now actually)

[Bolton Bailey]

Really? I should've waited.

[Junyan Xu]

Eric Rodriguez said:

(it's 40/hr now actually)

Haven't tried yet but from the description you'll be proving rather than formalizing the statements!

[Bolton Bailey]

Yeah just tried it (I saw several of my own statement formalizations!). Unfortunately, an hour is not really enough to formalize almost any of these, at least for me. I finally finished one by a big case bash, but when I went back to prolific, I got "You did not complete Proving mathematical problems in Lean on time and you were timed out" :neutral: .

[Bolton Bailey]

If the organizers of this want formalized statements as an end goal, I think they're much likelier to get them if they have people formalize their own statements. I spent the first forty minutes fighting the nat.card API (which someone else must have introduced, and which I am not familiar with) before giving up.

[Bolton Bailey]

I spent the next forty minutes trying to prove that sin x = 1 if and only if x is of the form pi/2 + 2pi k for integer k as a lemma to another question, but after seeing that I wasn't close to this and there were other things I needed, I gave up on this one too.

[Bolton Bailey]

I felt guilty to take their 40 bucks having not formalized anything, so I eventually clicked around until I found an easy one using nat.digits which was accomplishable using case bashing and linarith, but I feel this wasn't a very "human" proof. If they're looking to train an LLM based on this kind of data, I don't know if it will be very effective.

[Bolton Bailey]

Bolton Bailey said:

Really? I should've waited.

By the way, I shouldn't have complained about this, I see that my account has actually been credited for the ones I did previously. Thanks!

[Junyan Xu]

Bolton Bailey said:

If the organizers of this want formalized statements as an end goal, I think they're much likelier to get them if they have people formalize their own statements. I spent the first forty minutes fighting the nat.card API (which someone else must have introduced, and which I am not familiar with) before giving up.

I spent the next forty minutes trying to prove that sin x = 1 if and only if x is of the form pi/2 + 2pi k for integer k as a lemma to another question, but after seeing that I wasn't close to this and there were other things I needed, I gave up on this one too.

Yeah, even when formalizing (not proving) statements I often feel many are worth library support or discussion with the community to arrive at an agreed-upon/consensus formalization (e.g. a problem about two-player games, though one player only have a single option at each turn (so it's like oracle-querying ...)). Consider how much work was needed from @Joseph Myers to formalize IMO geometry problems! However, I think everyone signed a consent form preventing them from disclosing any problems or even their participation.

[Samara Zauhy]

Hey everyone! We realised there was a slight delay between users signing up to Prolific and getting the Lean study on their page, and we’re happy to say this has now been fixed. If you sign up using **THIS LINK**, you will be granted access to the study straight away (also updated on our original comms for new users to the thread).

Everyone who has already signed up should have full visibility of the first Lean 3 study, all you need to do is log in to your Prolific account. The first study (a Lean 3 test) takes around 50 minutes to complete and pays £21.61/hr. From this initial study you may also unlock further paid Lean 3 tasks, depending on your skill level!

We are constantly looking for ways to make our product and user experience better, so feel free to share feedback about the platform with us.

[Stuart Presnell]

Is there a strict time limit on the first study, or is 50 minutes just an estimated time to complete?

[Samara Zauhy]

@Stuart Presnell 50 minutes has been the average completion time so far! The max time allowed is 1 hour and 55 minutes .

[Stuart Presnell]

Thanks! Does unlocking further tasks depend on the time taken to complete the first study, or is it just based on successfully completing the test?

[Stuart Presnell]

I ask just because I feel like I'm a bit rusty with Lean 3 and I'm wondering whether I should practice to get back up to speed before starting the study.

[Samara Zauhy]

@Stuart Presnell Good question - this is based on skill level and not speed of completion, although you'd need to stick to the max allocated time.

[Samara Zauhy]

If you run over though you can still message the researcher and they might choose to manually approve the submission based on the responses!

[Stuart Presnell]

Great, thanks very much

[Samara Zauhy]

UPDATE: Lean 3 task reward has increased to £40/hr (previously £21.61/hr)! There are still places available, so if you're interested you can still sign up using **this link**. You will be taken to a Lean 3 study as soon as you signup. The study takes approx. 50 minutes to complete . From this initial study, you can unlock further Lean 3 tasks (also paying £40/hr), based on your skill-level!

If you have any questions, as always, feel free to DM me here or reply to the thread and I'll address them asap.

[Bulhwi Cha]

Hi Bulhwi,

Sorry, but we weren't able to verify your account and are therefore unable to offer you a place as a participant on Prolific.

Have a question? Contact our support team.

@Samara Zauhy Is there a reason Prolific can't verify my account?

[Samara Zauhy]

Hey @Bulhwi Cha, you should be approved now! Let me know if you need any help - if you signed through the link in this thread you should get the Lean 3 study straight away

[Bulhwi Cha]

PEC-SUB-0002

What does it mean?

Your IP address has been flagged by our system. We run multiple checks with IPs that include checking if the IP has been reported on other websites. You won't be able to take studies from that IP address for now but IPs are regularly reviewed so it could be unflagged in future.

@Samara Zauhy I can't start study due to this error.

[Paul Lezeau]

Bulhwi Cha said:

PEC-SUB-0002

What does it mean?

Your IP address has been flagged by our system. We run multiple checks with IPs that include checking if the IP has been reported on other websites. You won't be able to take studies from that IP address for now but IPs are regularly reviewed so it could be unflagged in future.

Samara Zauhy I can't start study due to this error.

I've run into this problem before, but changing networks (e.g. using mobile data) worked for me

[Samara Zauhy]

Hi @Bulhwi Cha, are you still having this issue? If so, I can have a look through your account and see what I can do! Echoing what @Paul Lezeau said, changing networks tend to be the best solution there!

[Bulhwi Cha]

@Samara Zauhy The error is gone now. Thanks!